1 /-
2 Copyright (c) 2015 Jeremy Avigad. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Jeremy Avigad, Robert Y. Lewis
5
6 The power operation on monoids and groups. We separate this from group, because it depends on
7 nat, which in turn depends on other parts of algebra.
8
9 We have "pow a n" for natural number powers, and "gpow a i" for integer powers. The notation
10 a^n is used for the first, but users can locally redefine it to gpow when needed.
11
12 Note: power adopts the convention that 0^0=1.
13 -/
14 import algebra.group
src └───────────┘
15 import data.int.basic data.list.basic
src └────────────┘ └─────────────┘
16
17 universes u v
18 variable {α : Type u}
19
20 /-- The power operation in a monoid. `a^n = a*a*...*a` n times. -/
21 def monoid.pow [monoid α] (a : α) : ℕ → α
id └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴
22 | 0 := 1
23 | (n+1) := a * monoid.pow n
id ┴┴ ┴ ┴ └────────┘
src ┴ ┴
typ ┴┴ ┴ ┴ └────────┘
24
25 def add_monoid.smul [add_monoid α] (n : ℕ) (a : α) : α :=
id └────────┘ ┴ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴ ┴ ┴
26 @monoid.pow (multiplicative α) _ a n
id └────────┘ └────────────┘ ┴ ┴ ┴
src └────────┘ └────────────┘
typ └────────┘ └────────────┘ ┴ ┴ ┴
doc └────────┘
27
28 precedence `•`:70
29 localized "infix ` • ` := add_monoid.smul" in add_monoid
30
31 @[priority 5] instance monoid.has_pow [monoid α] : has_pow α ℕ := ⟨monoid.pow⟩
id └────┘ ┴ └─────┘ ┴ ┴ └────────┘
src └────┘ └─────┘ ┴ └────────┘
typ └────┘ ┴ └─────┘ ┴ ┴ └────────┘
doc └────────┘
32
33 /- monoid -/
34 section monoid
35 variables [monoid α] {β : Type u} [add_monoid β]
id └────┘ └────────┘
src └────┘ └────────┘
typ └────┘ └────────┘
36
37 @[simp] theorem pow_zero (a : α) : a^0 = 1 := rfl
id ┴ ┴┴ ┴ └─┘
src ┴ ┴ └─┘
typ ┴ ┴┴ ┴ └─┘
doc └──┘
38 @[simp] theorem add_monoid.zero_smul (a : β) : 0 • a = 0 := rfl
id ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ └─┘
doc └──┘
39
40 theorem pow_succ (a : α) (n : ℕ) : a^(n+1) = a * a^n := rfl
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴ └─┘
41 theorem succ_smul (a : β) (n : ℕ) : (n+1)•a = a + n•a := rfl
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴ └─┘
42
43 @[simp] theorem pow_one (a : α) : a^1 = a := mul_one _
id ┴ ┴┴ ┴ ┴ └─────┘
src ┴ ┴ └─────┘
typ ┴ ┴┴ ┴ ┴ └─────┘
doc └──┘
44 @[simp] theorem add_monoid.one_smul (a : β) : 1•a = a := add_zero _
id ┴ ┴┴ ┴ ┴ └──────┘
src ┴ ┴ └──────┘
typ ┴ ┴┴ ┴ ┴ └──────┘
doc └──┘
45
46 theorem pow_mul_comm' (a : α) (n : ℕ) : a^n * a = a * a^n :=
id ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴
47 by induction n with n ih; [rw [pow_zero, one_mul, mul_one],
id ┴ ┴ └──────┘ └─────┘ └─────┘
src └────────┘ └────────┘ ┴└──┘└──────┘└┘└─────┘└┘└─────┘┴
typ └────────┘┴└────────┘ ┴└──┘└──────┘└┘└─────┘└┘└─────┘┴
doc └────────┘ └────────┘ └──┘ └┘ └┘ ┴
txt └────────┘ └────────┘ └──┘ └┘ └┘ ┴
par └────────┘ └────────┘ └──┘ └┘ └┘ ┴
pid ┴ ┴└───────┘ └┘ └┘ └┘ ┴
st └───────────────────────────┘└──────┘└───────┘└───────┘┴└─
48 rw [pow_succ, mul_assoc, ih]]
id └──────┘ └───────┘ └┘
src └──┘└──────┘└┘└───────┘└┘ ┴
typ └──┘└──────┘└┘└───────┘└┘└┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ─────┘└──────┘└─────────┘└──┘┴┴
49 theorem smul_add_comm' : ∀ (a : β) (n : ℕ), n•a + a = a + n•a :=
id ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴
50 @pow_mul_comm' (multiplicative β) _
id └───────────┘ └────────────┘ ┴
src └───────────┘ └────────────┘
typ └───────────┘ └────────────┘ ┴
51
52 theorem pow_succ' (a : α) (n : ℕ) : a^(n+1) = a^n * a :=
id ┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴
53 by rw [pow_succ, pow_mul_comm']
id └──────┘ └───────────┘
src └──┘└──────┘└┘└───────────┘└┘
typ └──┘└──────┘└┘└───────────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └───────────┘└─────────────┘┴┴
54 theorem succ_smul' (a : β) (n : ℕ) : (n+1)•a = n•a + a :=
id ┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴
55 by rw [succ_smul, smul_add_comm']
id └───────┘ └────────────┘
src └──┘└───────┘└┘└────────────┘└─
typ └──┘└───────┘└┘└────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────┘└──────────────┘┴└
56
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
57 theorem pow_two (a : α) : a^2 = a * a :=
id ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴
58 show a*(a*1)=a*a, by rw mul_one
id ┴┴ ┴┴ ┴┴┴┴ └─────┘
src ┴ ┴ ┴ ┴ └─┘└─────┘┴
typ ┴┴ ┴┴ ┴┴┴┴ └─┘└─────┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st └──────────┘
59 theorem two_smul (a : β) : 2•a = a + a :=
id ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴
60 show a+(a+0)=a+a, by rw add_zero
id ┴┴ ┴┴ ┴┴┴┴ └──────┘
src ┴ ┴ ┴ ┴ └─┘└──────┘└
typ ┴┴ ┴┴ ┴┴┴┴ └─┘└──────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └────────────
61
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
62 theorem pow_add (a : α) (m n : ℕ) : a^(m + n) = a^m * a^n :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
63 by induction n with n ih; [rw [add_zero, pow_zero, mul_one],
id ┴ ┴ └──────┘ └──────┘ └─────┘
src └────────┘ └────────┘ ┴└──┘└──────┘└┘└──────┘└┘└─────┘┴
typ └────────┘┴└────────┘ ┴└──┘└──────┘└┘└──────┘└┘└─────┘┴
doc └────────┘ └────────┘ └──┘ └┘ └┘ ┴
txt └────────┘ └────────┘ └──┘ └┘ └┘ ┴
par └────────┘ └────────┘ └──┘ └┘ └┘ ┴
pid ┴ ┴└───────┘ └┘ └┘ └┘ ┴
st └───────────────────────────┘└──────┘└────────┘└───────┘┴└─
64 rw [pow_succ, ← pow_mul_comm', ← mul_assoc, ← ih, ← pow_succ']]; refl
id └──────┘ └───────────┘ └───────┘ └┘ └───────┘
src └──┘└──────┘└──┘└───────────┘└──┘└───────┘└──┘ └──┘└───────┘┴ └───┘
typ └──┘└──────┘└──┘└───────────┘└──┘└───────┘└──┘└┘└──┘└───────┘┴ └───┘
doc └──┘ └──┘ └──┘ └──┘ └──┘ ┴ └───┘
txt └──┘ └──┘ └──┘ └──┘ └──┘ ┴ └───┘
par └──┘ └──┘ └──┘ └──┘ └──┘ ┴ └───┘
pid └┘ └──┘ └──┘ └──┘ └──┘ ┴ ┴
st ─────┘└──────┘└───────────────┘└───────────┘└────┘└───────────┘┴└──────┘
65 theorem add_monoid.add_smul : ∀ (a : β) (m n : ℕ), (m + n)•a = m•a + n•a :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
66 @pow_add (multiplicative β) _
id └─────┘ └────────────┘ ┴
src └─────┘ └────────────┘
typ └─────┘ └────────────┘ ┴
67
68 @[simp] theorem one_pow (n : ℕ) : (1 : α)^n = (1:α) :=
id ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴
doc └──┘
69 by induction n with n ih; [refl, rw [pow_succ, ih, one_mul]]
id ┴ ┴ └──────┘ └┘ └─────┘
src └────────┘ └────────┘ ┴└──┘ └──┘└──────┘└┘ └┘└─────┘┴
typ └────────┘┴└────────┘ ┴└──┘ └──┘└──────┘└┘└┘└┘└─────┘┴
doc └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ ┴
txt └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ ┴
par └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ ┴
pid ┴ ┴└───────┘ └┘ └┘ └┘ ┴
st └─────────────────────────────────┘└──────┘└──┘└───────┘┴┴
70 @[simp] theorem add_monoid.smul_zero (n : ℕ) : n•(0 : β) = (0:β) :=
id ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴
doc └──┘
71 by induction n with n ih; [refl, rw [succ_smul, ih, zero_add]]
id ┴ ┴ └───────┘ └┘ └──────┘
src └────────┘ └────────┘ ┴└──┘ └──┘└───────┘└┘ └┘└──────┘┴
typ └────────┘┴└────────┘ ┴└──┘ └──┘└───────┘└┘└┘└┘└──────┘┴
doc └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ ┴
txt └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ ┴
par └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ ┴
pid ┴ ┴└───────┘ └┘ └┘ └┘ ┴
st └─────────────────────────────────┘└───────┘└──┘└────────┘┴┴
72
73 theorem pow_mul (a : α) (m n : ℕ) : a^(m * n) = (a^m)^n :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴
74 by induction n with n ih; [rw mul_zero, rw [nat.mul_succ, pow_add, pow_succ', ih]]; refl
id ┴ ┴ └──────┘ └──────────┘ └─────┘ └───────┘ └┘
src └────────┘ └────────┘ ┴└─┘└──────┘ └──┘└──────────┘└┘└─────┘└┘└───────┘└┘ ┴ └───┘
typ └────────┘┴└────────┘ ┴└─┘└──────┘ └──┘└──────────┘└┘└─────┘└┘└───────┘└┘└┘┴ └───┘
doc └────────┘ └────────┘ └─┘ └──┘ └┘ └┘ └┘ ┴ └───┘
txt └────────┘ └────────┘ └─┘ └──┘ └┘ └┘ └┘ ┴ └───┘
par └────────┘ └────────┘ └─┘ └──┘ └┘ └┘ └┘ ┴ └───┘
pid ┴ ┴└───────┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴
st └──────────────────────────┘└──────┘└────┘└──────────┘└───────┘└─────────┘└──┘┴└──────┘
75 theorem add_monoid.mul_smul' : ∀ (a : β) (m n : ℕ), m * n • a = n•(m•a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴┴
76 @pow_mul (multiplicative β) _
id └─────┘ └────────────┘ ┴
src └─────┘ └────────────┘
typ └─────┘ └────────────┘ ┴
77
78 theorem pow_mul' (a : α) (m n : ℕ) : a^(m * n) = (a^n)^m :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴
79 by rw [mul_comm, pow_mul]
id └──────┘ └─────┘
src └──┘└──────┘└┘└─────┘└┘
typ └──┘└──────┘└┘└─────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └───────────┘└───────┘┴┴
80 theorem add_monoid.mul_smul (a : β) (m n : ℕ) : m * n • a = m•(n•a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴┴
81 by rw [mul_comm, add_monoid.mul_smul']
id └──────┘ └──────────────────┘
src └──┘└──────┘└┘└──────────────────┘└─
typ └──┘└──────┘└┘└──────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────┘└────────────────────┘┴└
82
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
83 @[simp] theorem add_monoid.smul_one [has_one β] : ∀ n : ℕ, n • (1 : β) = n :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
84 nat.eq_cast _ (add_monoid.zero_smul _) (add_monoid.one_smul _) (add_monoid.add_smul _)
id └─────────┘ └──────────────────┘ └─────────────────┘ └─────────────────┘
src └─────────┘ └──────────────────┘ └─────────────────┘ └─────────────────┘
typ └─────────┘ └──────────────────┘ └─────────────────┘ └─────────────────┘
85
86 theorem pow_bit0 (a : α) (n : ℕ) : a ^ bit0 n = a^n * a^n := pow_add _ _ _
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └─────┘
src ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └─────┘
87 theorem bit0_smul (a : β) (n : ℕ) : bit0 n • a = n•a + n•a := add_monoid.add_smul _ _ _
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └─────────────────┘
src ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └─────────────────┘
88
89 theorem pow_bit1 (a : α) (n : ℕ) : a ^ bit1 n = a^n * a^n * a :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴
90 by rw [bit1, pow_succ', pow_bit0]
id └──┘ └───────┘ └──────┘
src └──┘└──┘└┘└───────┘└┘└──────┘└┘
typ └──┘└──┘└┘└───────┘└┘└──────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st └───────┘└─────────┘└────────┘┴┴
91 theorem bit1_smul : ∀ (a : β) (n : ℕ), bit1 n • a = n•a + n•a + a :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴
92 @pow_bit1 (multiplicative β) _
id └──────┘ └────────────┘ ┴
src └──────┘ └────────────┘
typ └──────┘ └────────────┘ ┴
93
94 theorem pow_mul_comm (a : α) (m n : ℕ) : a^m * a^n = a^n * a^m :=
id ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴
95 by rw [←pow_add, ←pow_add, add_comm]
id └─────┘ └─────┘ └──────┘
src └───┘└─────┘└─┘└─────┘└┘└──────┘└┘
typ └───┘└─────┘└─┘└─────┘└┘└──────┘└┘
doc └───┘ └─┘ └┘ └┘
txt └───┘ └─┘ └┘ └┘
par └───┘ └─┘ └┘ └┘
pid └─┘ └─┘ └┘ ┴┴
st └───────────┘└────────┘└────────┘┴┴
96 theorem smul_add_comm : ∀ (a : β) (m n : ℕ), m•a + n•a = n•a + m•a :=
id ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴
97 @pow_mul_comm (multiplicative β) _
id └──────────┘ └────────────┘ ┴
src └──────────┘ └────────────┘
typ └──────────┘ └────────────┘ ┴
98
99 @[simp] theorem list.prod_repeat (a : α) (n : ℕ) : (list.repeat a n).prod = a ^ n :=
id ┴ ┴ └─────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src ┴ └─────────┘ └──┘ ┴ ┴
typ ┴ ┴ └─────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘ └──┘
100 by induction n with n ih; [refl, rw [list.repeat_succ, list.prod_cons, ih]]; refl
id ┴ ┴ └──────────────┘ └────────────┘ └┘
src └────────┘ └────────┘ ┴└──┘ └──┘└──────────────┘└┘└────────────┘└┘ ┴ └───┘
typ └────────┘┴└────────┘ ┴└──┘ └──┘└──────────────┘└┘└────────────┘└┘└┘┴ └───┘
doc └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ ┴ └───┘
txt └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ ┴ └───┘
par └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ ┴ └───┘
pid ┴ ┴└───────┘ └┘ └┘ └┘ ┴ ┴
st └─────────────────────────────────┘└──────────────┘└──────────────┘└──┘┴└──────┘
101 @[simp] theorem list.sum_repeat : ∀ (a : β) (n : ℕ), (list.repeat a n).sum = n • a :=
id ┴ ┴ └─────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ └─────────┘ └─┘ ┴ ┴
typ ┴ ┴ └─────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
doc └──┘ └─┘
102 @list.prod_repeat (multiplicative β) _
id └──────────────┘ └────────────┘ ┴
src └──────────────┘ └────────────┘
typ └──────────────┘ └────────────┘ ┴
103
104 @[simp] lemma units.coe_pow (u : units α) (n : ℕ) : ((u ^ n : units α) : α) = u ^ n :=
id └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
105 by induction n; simp [*, pow_succ]
id ┴ └──────┘
src └────────┘ └───────┘└──────┘└─
typ └────────┘┴ └───────┘└──────┘└─
doc └────────┘ └───────┘ └─
txt └────────┘ └───────┘ └─
par └────────┘ └───────┘ └─
pid ┴ ┴└──┘ ┴└
st └────────────────────────────────
106
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
107 end monoid
108
109 namespace is_monoid_hom
110 variables {β : Type v} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f]
id └────┘ └────┘ └───────────┘
src └────┘ └────┘ └───────────┘
typ └────┘ └────┘ └───────────┘
doc └───────────┘
111
112 theorem map_pow (a : α) : ∀(n : ℕ), f (a ^ n) = (f a) ^ n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
113 | 0 := is_monoid_hom.map_one f
id └───────────────────┘ ┴
src └───────────────────┘
typ └───────────────────┘ ┴
114 | (nat.succ n) := by rw [pow_succ, is_monoid_hom.map_mul f, map_pow n]; refl
id └──────┘ └──────┘ └───────────────────┘ ┴ └─────┘ ┴
src └──────┘ └──┘└──────┘└┘└───────────────────┘┴ └┘ ┴ ┴ └────
typ └──────┘ └──┘└──────┘└┘└───────────────────┘┴┴└┘└─────┘┴┴┴ └────
doc └──┘ └┘└───────────────────┘┴ └┘ ┴ ┴ └────
txt └──┘ └┘ ┴ └┘ ┴ ┴ └────
par └──┘ └┘ ┴ └┘ ┴ ┴ └────
pid └┘ └┘ ┴ └┘ ┴ ┴ └
st └───────────┘└───────────────────────┘└─────────┘┴└──────
115
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
116 end is_monoid_hom
117
118 namespace is_add_monoid_hom
119 variables {β : Type*} [add_monoid α] [add_monoid β] (f : α → β) [is_add_monoid_hom f]
id └────────┘ └────────┘ └───────────────┘
src └────────┘ └────────┘ └───────────────┘
typ └────────┘ └────────┘ └───────────────┘
doc └───────────────┘
120
121 theorem map_smul (a : α) : ∀(n : ℕ), f (n • a) = n • (f a)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
122 | 0 := is_add_monoid_hom.map_zero f
id └────────────────────────┘ ┴
src └────────────────────────┘
typ └────────────────────────┘ ┴
123 | (nat.succ n) := by rw [succ_smul, is_add_monoid_hom.map_add f, map_smul n]; refl
id └──────┘ └───────┘ └───────────────────────┘ ┴ └──────┘ ┴
src └──────┘ └──┘└───────┘└┘└───────────────────────┘┴ └┘ ┴ ┴ └────
typ └──────┘ └──┘└───────┘└┘└───────────────────────┘┴┴└┘└──────┘┴┴┴ └────
doc └──┘ └┘ ┴ └┘ ┴ ┴ └────
txt └──┘ └┘ ┴ └┘ ┴ ┴ └────
par └──┘ └┘ ┴ └┘ ┴ ┴ └────
pid └┘ └┘ ┴ └┘ ┴ ┴ └
st └────────────┘└───────────────────────────┘└──────────┘┴└──────
124
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
125 end is_add_monoid_hom
126
127 namespace monoid_hom
128 variables {β : Type v} [monoid α] [monoid β] (f : α →* β)
id └────┘ └────┘ └┘
src └────┘ └────┘ └┘
typ └────┘ └────┘ └┘
doc └┘
129
130 @[simp] theorem map_pow (a : α) : ∀(n : ℕ), f (a ^ n) = (f a) ^ n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
131 | 0 := f.map_one
id ┴└──────┘
src └──────┘
typ ┴└──────┘
doc └──────┘
132 | (nat.succ n) := by rw [pow_succ, f.map_mul, map_pow n]; refl
id └──────┘ └──────┘ └─────┘ ┴
src └──────┘ └──┘└──────┘└┘ └┘ ┴ ┴ └────
typ └──────┘ └──┘└──────┘└┘└───────┘└┘└─────┘┴┴┴ └────
doc └──┘ └┘ └┘ ┴ ┴ └────
txt └──┘ └┘ └┘ ┴ ┴ └────
par └──┘ └┘ └┘ ┴ ┴ └────
pid └┘ └┘ └┘ ┴ ┴ └
st └───────────┘└─────────┘└─────────┘┴└──────
133
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
134 end monoid_hom
135
136 namespace add_monoid_hom
137 variables {β : Type*} [add_monoid α] [add_monoid β] (f : α →+ β)
id └────────┘ └────────┘ └┘
src └────────┘ └────────┘ └┘
typ └────────┘ └────────┘ └┘
doc └┘
138
139 @[simp] theorem map_smul (a : α) : ∀(n : ℕ), f (n • a) = n • (f a)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
140 | 0 := f.map_zero
id ┴└───────┘
src └───────┘
typ ┴└───────┘
141 | (nat.succ n) := by rw [succ_smul, f.map_add, map_smul n]; refl
id └──────┘ └───────┘ └──────┘ ┴
src └──────┘ └──┘└───────┘└┘ └┘ ┴ ┴ └────
typ └──────┘ └──┘└───────┘└┘└───────┘└┘└──────┘┴┴┴ └────
doc └──┘ └┘ └┘ ┴ ┴ └────
txt └──┘ └┘ └┘ ┴ ┴ └────
par └──┘ └┘ └┘ ┴ ┴ └────
pid └┘ └┘ └┘ ┴ ┴ └
st └────────────┘└─────────┘└──────────┘┴└──────
142
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
143 end add_monoid_hom
144
145 @[simp] theorem nat.pow_eq_pow (p q : ℕ) :
id ┴
src ┴
typ ┴
doc └──┘
146 @has_pow.pow _ _ monoid.has_pow p q = p ^ q :=
id └─────────┘ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ └────────────┘ ┴ ┴
typ └─────────┘ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
147 by induction q with q ih; [refl, rw [nat.pow_succ, pow_succ, mul_comm, ih]]
id ┴ ┴ └──────────┘ └──────┘ └──────┘ └┘
src └────────┘ └────────┘ ┴└──┘ └──┘└──────────┘└┘└──────┘└┘└──────┘└┘ ┴
typ └────────┘┴└────────┘ ┴└──┘ └──┘└──────────┘└┘└──────┘└┘└──────┘└┘└┘┴
doc └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ └┘ ┴
txt └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ └┘ ┴
par └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ └┘ ┴
pid ┴ ┴└───────┘ └┘ └┘ └┘ └┘ ┴
st └─────────────────────────────────┘└──────────┘└────────┘└────────┘└──┘┴┴
148
149 @[simp] theorem nat.smul_eq_mul (m n : ℕ) : m • n = m * n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
150 by induction m with m ih; [rw [add_monoid.zero_smul, zero_mul],
id ┴ ┴ └──────────────────┘ └──────┘
src └────────┘ └────────┘ ┴└──┘└──────────────────┘└┘└──────┘┴
typ └────────┘┴└────────┘ ┴└──┘└──────────────────┘└┘└──────┘┴
doc └────────┘ └────────┘ └──┘ └┘ ┴
txt └────────┘ └────────┘ └──┘ └┘ ┴
par └────────┘ └────────┘ └──┘ └┘ ┴
pid ┴ ┴└───────┘ └┘ └┘ ┴
st └───────────────────────────┘└──────────────────┘└────────┘┴└─
151 rw [succ_smul', ih, nat.succ_mul]]
id └────────┘ └┘ └──────────┘
src └──┘└────────┘└┘ └┘└──────────┘┴
typ └──┘└────────┘└┘└┘└┘└──────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ─────┘└────────┘└──┘└────────────┘┴┴
152
153 /- commutative monoid -/
154
155 section comm_monoid
156 variables [comm_monoid α] {β : Type*} [add_comm_monoid β]
id └─────────┘ └─────────────┘
src └─────────┘ └─────────────┘
typ └─────────┘ └─────────────┘
157
158 theorem mul_pow (a b : α) (n : ℕ) : (a * b)^n = a^n * b^n :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
159 by induction n with n ih; [exact (mul_one _).symm,
id ┴ ┴ └─────┘
src └────────┘ └────────┘ ┴└────┘ └─────┘└──────┘
typ └────────┘┴└────────┘ ┴└────┘ └─────┘└──────┘
doc └────────┘ └────────┘ └────┘ └──────┘
txt └────────┘ └────────┘ └────┘ └──────┘
par └────────┘ └────────┘ └────┘ └──────┘
pid ┴ ┴└───────┘ ┴ └─────┘┴
st └────────────────────────────────────────────────
160 simp only [pow_succ, ih, mul_assoc, mul_left_comm]]
id └──────┘ └┘ └───────┘ └───────────┘
src └─────────┘└──────┘└┘ └┘└───────┘└┘└───────────┘┴
typ └─────────┘└──────┘└┘└┘└┘└───────┘└┘└───────────┘┴
doc └─────────┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────┘
161 theorem add_monoid.smul_add : ∀ (a b : β) (n : ℕ), n•(a + b) = n•a + n•b :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
162 @mul_pow (multiplicative β) _
id └─────┘ └────────────┘ ┴
src └─────┘ └────────────┘
typ └─────┘ └────────────┘ ┴
163
164 instance pow.is_monoid_hom (n : ℕ) : is_monoid_hom ((^ n) : α → α) :=
id ┴ └───────────┘ ┴ ┴ ┴ ┴
src ┴ └───────────┘ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc └───────────┘
165 { map_mul := λ _ _, mul_pow _ _ _, map_one := one_pow _ }
id ┴ ┴ └─────┘ └─────┘
src └─────┘ └─────┘
typ ┴ ┴ └─────┘ └─────┘
166
167 instance add_monoid.smul.is_add_monoid_hom (n : ℕ) : is_add_monoid_hom (add_monoid.smul n : β → β) :=
id ┴ └───────────────┘ └─────────────┘ ┴ ┴ ┴
src ┴ └───────────────┘ └─────────────┘
typ ┴ └───────────────┘ └─────────────┘ ┴ ┴ ┴
doc └───────────────┘
168 { map_add := λ _ _, add_monoid.smul_add _ _ _, map_zero := add_monoid.smul_zero _ }
id ┴ ┴ └─────────────────┘ └──────────────────┘
src └─────────────────┘ └──────────────────┘
typ ┴ ┴ └─────────────────┘ └──────────────────┘
169
170 end comm_monoid
171
172 section group
173 variables [group α] {β : Type*} [add_group β]
id └───┘ └───────┘
src └───┘ └───────┘
typ └───┘ └───────┘
174
175 section nat
176
177 @[simp] theorem inv_pow (a : α) (n : ℕ) : (a⁻¹)^n = (a^n)⁻¹ :=
id ┴ ┴ ┴└┘ ┴┴ ┴ ┴┴┴ └┘
src ┴ └┘ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴└┘ ┴┴ ┴ ┴┴┴ └┘
doc └──┘
178 by induction n with n ih; [exact one_inv.symm,
id ┴ ┴ └──────────┘
src └────────┘ └────────┘ ┴└────┘└──────────┘
typ └────────┘┴└────────┘ ┴└────┘└──────────┘
doc └────────┘ └────────┘ └────┘
txt └────────┘ └────────┘ └────┘
par └────────┘ └────────┘ └────┘
pid ┴ ┴└───────┘ ┴
st └────────────────────────────────────────────
179 rw [pow_succ', pow_succ, ih, mul_inv_rev]]
id └───────┘ └──────┘ └┘ └─────────┘
src └──┘└───────┘└┘└──────┘└┘ └┘└─────────┘┴
typ └──┘└───────┘└┘└──────┘└┘└┘└┘└─────────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ─────┘└───────┘└────────┘└──┘└───────────┘┴┴
180 @[simp] theorem add_monoid.neg_smul : ∀ (a : β) (n : ℕ), n•(-a) = -(n•a) :=
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴┴
doc └──┘
181 @inv_pow (multiplicative β) _
id └─────┘ └────────────┘ ┴
src └─────┘ └────────────┘
typ └─────┘ └────────────┘ ┴
182
183 theorem pow_sub (a : α) {m n : ℕ} (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └┘
184 have h1 : m - n + n = m, from nat.sub_add_cancel h,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴
src ┴ ┴ ┴ └────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴
185 have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1],
id ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └─────┘ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ └───┘└─────┘└┘ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └───┘└─────┘└┘└┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └─┘ └┘ ┴
st └───────────┘└──┘┴
186 eq_mul_inv_of_mul_eq h2
id └──────────────────┘ └┘
src └──────────────────┘
typ └──────────────────┘ └┘
187 theorem add_monoid.smul_sub : ∀ (a : β) {m n : ℕ}, n ≤ m → (m - n)•a = m•a - n•a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
188 @pow_sub (multiplicative β) _
id └─────┘ └────────────┘ ┴
src └─────┘ └────────────┘
typ └─────┘ └────────────┘ ┴
189
190 theorem pow_inv_comm (a : α) (m n : ℕ) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m :=
id ┴ ┴ ┴└┘ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴└┘ ┴┴
src ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴└┘ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴└┘ ┴┴
191 by rw inv_pow; exact inv_comm_of_comm (pow_mul_comm _ _ _)
id └─────┘ └──────────────┘ └──────────┘
src └─┘└─────┘ └────┘└──────────────┘┴ └──────────┘└──────┘
typ └─┘└─────┘ └────┘└──────────────┘┴ └──────────┘└──────┘
doc └─┘ └────┘ ┴ └──────┘
txt └─┘ └────┘ ┴ └──────┘
par └─┘ └────┘ ┴ └──────┘
pid ┴ ┴ ┴ └─────┘┴
st └───────────────────────────────────────────────────────┘
192 theorem add_monoid.smul_neg_comm : ∀ (a : β) (m n : ℕ), m•(-a) + n•a = n•a + m•(-a) :=
id ┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴ ┴┴
193 @pow_inv_comm (multiplicative β) _
id └──────────┘ └────────────┘ ┴
src └──────────┘ └────────────┘
typ └──────────┘ └────────────┘ ┴
194 end nat
195
196 open int
197
198 /--
199 The power operation in a group. This extends `monoid.pow` to negative integers
200 with the definition `a^(-n) = (a^n)⁻¹`.
201 -/
202 def gpow (a : α) : ℤ → α
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
203 | (of_nat n) := a^n
id └────┘ ┴ ┴┴
src └────┘ ┴
typ └────┘ ┴ ┴┴
204 | -[1+n] := (a^(nat.succ n))⁻¹
id └──┘┴┴ ┴┴ └──────┘ └┘
src └──┘ ┴ ┴ └──────┘ └┘
typ └──┘┴┴ ┴┴ └──────┘ └┘
205
206 def gsmul (n : ℤ) (a : β) : β :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
207 @gpow (multiplicative β) _ a n
id └──┘ └────────────┘ ┴ ┴ ┴
src └──┘ └────────────┘
typ └──┘ └────────────┘ ┴ ┴ ┴
doc └──┘
208
209 @[priority 10] instance group.has_pow : has_pow α ℤ := ⟨gpow⟩
id └─────┘ ┴ ┴ └──┘
src └─────┘ ┴ └──┘
typ └─────┘ ┴ ┴ └──┘
doc └──┘
210
211 localized "infix ` • `:70 := gsmul" in add_group
212 localized "infix ` •ℕ `:70 := add_monoid.smul" in smul
213 localized "infix ` •ℤ `:70 := gsmul" in smul
214
215 @[simp] theorem gpow_coe_nat (a : α) (n : ℕ) : a ^ (n:ℤ) = a ^ n := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
216 @[simp] theorem gsmul_coe_nat (a : β) (n : ℕ) : (n:ℤ) • a = n •ℕ a := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
src ┴ ┴ ┴ ┴ └┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
doc └──┘
217
218 @[simp] theorem gpow_of_nat (a : α) (n : ℕ) : a ^ of_nat n = a ^ n := rfl
id ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ └────┘ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
219 @[simp] theorem gsmul_of_nat (a : β) (n : ℕ) : of_nat n • a = n •ℕ a := rfl
id ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
src ┴ └────┘ ┴ ┴ └┘ └─┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
doc └──┘
220
221 @[simp] theorem gpow_neg_succ (a : α) (n : ℕ) : a ^ -[1+n] = (a ^ n.succ)⁻¹ := rfl
id ┴ ┴ ┴ ┴ └──┘┴┴ ┴ ┴ ┴ ┴└───┘ └┘ └─┘
src ┴ ┴ └──┘ ┴ ┴ ┴ └───┘ └┘ └─┘
typ ┴ ┴ ┴ ┴ └──┘┴┴ ┴ ┴ ┴ ┴└───┘ └┘ └─┘
doc └──┘
222 @[simp] theorem gsmul_neg_succ (a : β) (n : ℕ) : -[1+n] • a = - (n.succ •ℕ a) := rfl
id ┴ ┴ └──┘┴┴ ┴ ┴ ┴ ┴ ┴└───┘ └┘ ┴ └─┘
src ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ └┘ └─┘
typ ┴ ┴ └──┘┴┴ ┴ ┴ ┴ ┴ ┴└───┘ └┘ ┴ └─┘
doc └──┘
223
224 local attribute [ematch] le_of_lt
id └──────┘
src └────┘ └──────┘
typ └──────┘
doc └────┘
225 open nat
226
227 @[simp] theorem gpow_zero (a : α) : a ^ (0:ℤ) = 1 := rfl
id ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
228 @[simp] theorem zero_gsmul (a : β) : (0:ℤ) • a = 0 := rfl
id ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
229
230 @[simp] theorem gpow_one (a : α) : a ^ (1:ℤ) = a := mul_one _
id ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └──┘
231 @[simp] theorem one_gsmul (a : β) : (1:ℤ) • a = a := add_zero _
id ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
doc └──┘
232
233 @[simp] theorem one_gpow : ∀ (n : ℤ), (1 : α) ^ n = 1
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
234 | (n : ℕ) := one_pow _
id ┴ └─────┘
src ┴ └─────┘
typ ┴ └─────┘
235 | -[1+ n] := show _⁻¹=(1:α), by rw [_root_.one_pow, one_inv]
id └──┘ ┴ └┘┴ ┴ └────────────┘ └─────┘
src └──┘ ┴ └┘┴ └──┘└────────────┘└┘└─────┘└┘
typ └──┘ ┴ └┘┴ ┴ └──┘└────────────┘└┘└─────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └─────────────────┘└───────┘┴┴
236 @[simp] theorem gsmul_zero : ∀ (n : ℤ), n • (0 : β) = 0 :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
237 @one_gpow (multiplicative β) _
id └──────┘ └────────────┘ ┴
src └──────┘ └────────────┘
typ └──────┘ └────────────┘ ┴
238
239 @[simp] theorem gpow_neg (a : α) : ∀ (n : ℤ), a ^ -n = (a ^ n)⁻¹
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
doc └──┘
240 | (n+1:ℕ) := rfl
id ┴ ┴ └─┘
src ┴ ┴ └─┘
typ ┴ ┴ └─┘
241 | 0 := one_inv.symm
id └─────┘└───┘
src └─────┘└───┘
typ └─────┘└───┘
242 | -[1+ n] := (inv_inv _).symm
id └──┘ ┴ └─────┘ └──┘
src └──┘ ┴ └─────┘ └──┘
typ └──┘ ┴ └─────┘ └──┘
243
244 @[simp] theorem neg_gsmul : ∀ (a : β) (n : ℤ), -n • a = -(n • a) :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
245 @gpow_neg (multiplicative β) _
id └──────┘ └────────────┘ ┴
src └──────┘ └────────────┘
typ └──────┘ └────────────┘ ┴
246
247 theorem gpow_neg_one (x : α) : x ^ (-1:ℤ) = x⁻¹ := congr_arg has_inv.inv $ pow_one x
id ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ └───────┘ └─────────┘ └─────┘ ┴
src ┴ ┴ ┴ ┴ └┘ └───────┘ └─────────┘ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ └───────┘ └─────────┘ └─────┘ ┴
248 theorem neg_one_gsmul (x : β) : (-1:ℤ) • x = -x := congr_arg has_neg.neg $ add_monoid.one_smul x
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └───────┘ └─────────┘ └─────────────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └─────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └───────┘ └─────────┘ └─────────────────┘ ┴
249
250 theorem gsmul_one [has_one β] (n : ℤ) : n • (1 : β) = n :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
251 begin
st └─────
252 cases n,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────┘└─
253 { rw [gsmul_of_nat, add_monoid.smul_one, int.cast_of_nat] },
id └──────────┘ └─────────────────┘ └─────────────┘
src └──┘└──────────┘└┘└─────────────────┘└┘└─────────────┘└┘
typ └──┘└──────────┘└┘└─────────────────┘└┘└─────────────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ───┘└──────────────┘└───────────────────┘└───────────────┘┴┴└┘└
254 { rw [gsmul_neg_succ, add_monoid.smul_one, int.cast_neg_succ_of_nat, nat.cast_succ] }
id └────────────┘ └─────────────────┘ └──────────────────────┘ └───────────┘
src └──┘└────────────┘└┘└─────────────────┘└┘└──────────────────────┘└┘└───────────┘└┘
typ └──┘└────────────┘└┘└─────────────────┘└┘└──────────────────────┘└┘└───────────┘└┘
doc └──┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ ┴┴
st ─────────────────────┘└───────────────────┘└────────────────────────┘└─────────────┘┴┴└─
255 end
st ──┘
256
257 theorem inv_gpow (a : α) : ∀n:ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
id ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src ┴ └┘ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
258 | (n : ℕ) := inv_pow a n
id ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ └─────┘ ┴
259 | -[1+ n] := congr_arg has_inv.inv $ inv_pow a (n+1)
id └──┘ ┴┴ └───────┘ └─────────┘ └─────┘ ┴ ┴
src └──┘ ┴ └───────┘ └─────────┘ └─────┘ ┴
typ └──┘ ┴┴ └───────┘ └─────────┘ └─────┘ ┴ ┴
260
261 private lemma gpow_add_aux (a : α) (m n : nat) :
id ┴ └─┘
src └─┘
typ ┴ └─┘
262 a ^ ((of_nat m) + -[1+n]) = a ^ of_nat m * a ^ -[1+n] :=
id ┴ ┴ └────┘ ┴ ┴ └──┘┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘┴┴
src ┴ └────┘ ┴ └──┘ ┴ ┴ ┴ └────┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ └──┘┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘┴┴
263 or.elim (nat.lt_or_ge m (nat.succ n))
id └─────┘ └──────────┘ ┴ └──────┘ ┴
src └─────┘ └──────────┘ └──────┘
typ └─────┘ └──────────┘ ┴ └──────┘ ┴
264 (assume h1 : m < succ n,
id ┴ ┴ └──┘ ┴
src ┴ └──┘
typ ┴ ┴ └──┘ ┴
265 have h2 : m ≤ n, from le_of_lt_succ h1,
id ┴ ┴ ┴ └───────────┘ └┘
src ┴ └───────────┘
typ ┴ ┴ ┴ └───────────┘ └┘
266 suffices a ^ -[1+ n-m] = a ^ of_nat m * a ^ -[1+n],
id ┴ ┴ └──┘ ┴┴┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘┴┴
src ┴ └──┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ └──┘ ┴┴┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘┴┴
267 by rwa [of_nat_add_neg_succ_of_nat_of_lt h1],
id └──────────────────────────────┘ └┘
src └───┘└──────────────────────────────┘┴ ┴
typ └───┘└──────────────────────────────┘┴└┘┴
doc └───┘ ┴ ┴
txt └───┘ ┴ ┴
par └───┘ ┴ ┴
pid └┘ ┴ ┴
st └───────────────────────────────────────┘┴
268 show (a ^ nat.succ (n - m))⁻¹ = a ^ of_nat m * a ^ -[1+n],
id ┴ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘┴┴
src ┴ └──────┘ ┴ └┘ ┴ ┴ └────┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘┴┴
269 by rw [← succ_sub h2, pow_sub _ (le_of_lt h1), mul_inv_rev, inv_inv]; refl)
id └──────┘ └┘ └─────┘ └──────┘ └┘ └─────────┘ └─────┘
src └────┘└──────┘┴ └┘└─────┘└─┘ └──────┘┴ └─┘└─────────┘└┘└─────┘┴ └──┘
typ └────┘└──────┘┴└┘└┘└─────┘└─┘ └──────┘┴└┘└─┘└─────────┘└┘└─────┘┴ └──┘
doc └────┘ ┴ └┘ └─┘ ┴ └─┘ └┘ ┴ └──┘
txt └────┘ ┴ └┘ └─┘ ┴ └─┘ └┘ ┴ └──┘
par └────┘ ┴ └┘ └─┘ ┴ └─┘ └┘ ┴ └──┘
pid └──┘ ┴ └┘ └─┘ ┴ └─┘ └┘ ┴
st └────────────────┘└───────────────────────┘└───────────┘└───────┘┴└────┘
270 (assume : m ≥ succ n,
id ┴ ┴ └──┘ ┴
src ┴ └──┘
typ ┴ ┴ └──┘ ┴
271 suffices a ^ (of_nat (m - succ n)) = (a ^ (of_nat m)) * (a ^ -[1+ n]),
id ┴ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴┴
src ┴ └────┘ ┴ └──┘ ┴ ┴ └────┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴┴
272 by rw [of_nat_add_neg_succ_of_nat_of_ge]; assumption,
id └──────────────────────────────┘
src └──┘└──────────────────────────────┘┴ └────────┘
typ └──┘└──────────────────────────────┘┴ └────────┘
doc └──┘ ┴ └────────┘
txt └──┘ ┴ └────────┘
par └──┘ ┴ └────────┘
pid └┘ ┴
st └───────────────────────────────────┘┴└──────────┘
273 suffices a ^ (m - succ n) = a ^ m * (a ^ n.succ)⁻¹, from this,
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ └┘ └──┘
src ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ └┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ └┘ └──┘
274 by rw pow_sub; assumption)
id └─────┘
src └─┘└─────┘ └────────┘
typ └─┘└─────┘ └────────┘
doc └─┘ └────────┘
txt └─┘ └────────┘
par └─┘ └────────┘
pid ┴
st └─────────────────────┘
275
276 theorem gpow_add (a : α) : ∀ (i j : ℤ), a ^ (i + j) = a ^ i * a ^ j
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
277 | (of_nat m) (of_nat n) := pow_add _ _ _
id └────┘ └─────┘
src └────┘ └─────┘
typ └────┘ └─────┘
278 | (of_nat m) -[1+n] := gpow_add_aux _ _ _
id └────┘ └──┘ ┴ └──────────┘
src └────┘ └──┘ ┴ └──────────┘
typ └────┘ └──┘ ┴ └──────────┘
279 | -[1+m] (of_nat n) := by rw [add_comm, gpow_add_aux,
id └──┘ ┴ └────┘ └──────┘ └──────────┘
src └──┘ ┴ └────┘ └──┘└──────┘└┘└──────────┘└─
typ └──┘ ┴ └────┘ └──┘└──────┘└┘└──────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ └─
st └───────────┘└────────────┘└─
280 gpow_neg_succ, gpow_of_nat, ← inv_pow, ← pow_inv_comm]
id └───────────┘ └─────────┘ └─────┘ └──────────┘
src ─┘└───────────┘└┘└─────────┘└──┘└─────┘└──┘└──────────┘└┘
typ ─┘└───────────┘└┘└─────────┘└──┘└─────┘└──┘└──────────┘└┘
doc ─┘ └┘ └──┘ └──┘ └┘
txt ─┘ └┘ └──┘ └──┘ └┘
par ─┘ └┘ └──┘ └──┘ └┘
pid ─┘ └┘ └──┘ └──┘ ┴┴
st ──────────────┘└───────────┘└─────────┘└──────────────┘┴┴
281 | -[1+m] -[1+n] :=
id └──┘┴┴ └──┘┴┴
src └──┘ ┴ └──┘ ┴
typ └──┘┴┴ └──┘┴┴
282 suffices (a ^ (m + succ (succ n)))⁻¹ = (a ^ m.succ)⁻¹ * (a ^ n.succ)⁻¹, from this,
id ┴ ┴ ┴ └──┘ └──┘ └┘ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ ┴ └───┘ └┘ └──┘
src ┴ ┴ └──┘ └──┘ └┘ ┴ ┴ └───┘ └┘ ┴ ┴ └───┘ └┘
typ ┴ ┴ ┴ └──┘ └──┘ └┘ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ ┴ └───┘ └┘ └──┘
283 by rw [← succ_add_eq_succ_add, add_comm, _root_.pow_add, mul_inv_rev]
id └──────────────────┘ └──────┘ └────────────┘ └─────────┘
src └────┘└──────────────────┘└┘└──────┘└┘└────────────┘└┘└─────────┘└─
typ └────┘└──────────────────┘└┘└──────┘└┘└────────────┘└┘└─────────┘└─
doc └────┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └─
pid └──┘ └┘ └┘ └┘ ┴└
st └─────────────────────────┘└────────┘└──────────────┘└───────────┘┴└
284
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
285 theorem add_gsmul : ∀ (a : β) (i j : ℤ), (i + j) • a = i • a + j • a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
286 @gpow_add (multiplicative β) _
id └──────┘ └────────────┘ ┴
src └──────┘ └────────────┘
typ └──────┘ └────────────┘ ┴
287
288 theorem gpow_add_one (a : α) (i : ℤ) : a ^ (i + 1) = a ^ i * a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
289 by rw [gpow_add, gpow_one]
id └──────┘ └──────┘
src └──┘└──────┘└┘└──────┘└┘
typ └──┘└──────┘└┘└──────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └───────────┘└────────┘┴┴
290 theorem add_one_gsmul : ∀ (a : β) (i : ℤ), (i + 1) • a = i • a + a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
291 @gpow_add_one (multiplicative β) _
id └──────────┘ └────────────┘ ┴
src └──────────┘ └────────────┘
typ └──────────┘ └────────────┘ ┴
292
293 theorem gpow_one_add (a : α) (i : ℤ) : a ^ (1 + i) = a * a ^ i :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
294 by rw [gpow_add, gpow_one]
id └──────┘ └──────┘
src └──┘└──────┘└┘└──────┘└┘
typ └──┘└──────┘└┘└──────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └───────────┘└────────┘┴┴
295 theorem one_add_gsmul : ∀ (a : β) (i : ℤ), (1 + i) • a = a + i • a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
296 @gpow_one_add (multiplicative β) _
id └──────────┘ └────────────┘ ┴
src └──────────┘ └────────────┘
typ └──────────┘ └────────────┘ ┴
297
298 theorem gpow_mul_comm (a : α) (i j : ℤ) : a ^ i * a ^ j = a ^ j * a ^ i :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
299 by rw [← gpow_add, ← gpow_add, add_comm]
id └──────┘ └──────┘ └──────┘
src └────┘└──────┘└──┘└──────┘└┘└──────┘└┘
typ └────┘└──────┘└──┘└──────┘└┘└──────┘└┘
doc └────┘ └──┘ └┘ └┘
txt └────┘ └──┘ └┘ └┘
par └────┘ └──┘ └┘ └┘
pid └──┘ └──┘ └┘ ┴┴
st └─────────────┘└──────────┘└────────┘┴┴
300 theorem gsmul_add_comm : ∀ (a : β) (i j), i • a + j • a = j • a + i • a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
301 @gpow_mul_comm (multiplicative β) _
id └───────────┘ └────────────┘ ┴
src └───────────┘ └────────────┘
typ └───────────┘ └────────────┘ ┴
302
303 theorem gpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
304 | (m : ℕ) (n : ℕ) := pow_mul _ _ _
id ┴ ┴ └─────┘
src ┴ ┴ └─────┘
typ ┴ ┴ └─────┘
305 | (m : ℕ) -[1+ n] := (gpow_neg _ (m * succ n)).trans $
id ┴ ┴ └──┘ ┴┴ └──────┘ ┴ └──┘ └───┘
src ┴ └──┘ ┴ └──────┘ ┴ └──┘ └───┘
typ ┴ ┴ └──┘ ┴┴ └──────┘ ┴ └──┘ └───┘
doc └──┘
306 show (a ^ (m * succ n))⁻¹ = _, by rw pow_mul; refl
id ┴ ┴ ┴ └──┘ └┘ ┴ └─────┘
src ┴ ┴ └──┘ └┘ ┴ └─┘└─────┘ └───┘
typ ┴ ┴ ┴ └──┘ └┘ ┴ └─┘└─────┘ └───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ ┴
st └────────────────┘
307 | -[1+ m] (n : ℕ) := (gpow_neg _ (succ m * n)).trans $
id └──┘ ┴┴ ┴ ┴ └──────┘ └──┘ ┴ └───┘
src └──┘ ┴ ┴ └──────┘ └──┘ ┴ └───┘
typ └──┘ ┴┴ ┴ ┴ └──────┘ └──┘ ┴ └───┘
doc └──┘
308 show (a ^ (m.succ * n))⁻¹ = _, by rw [pow_mul, ← inv_pow]; refl
id ┴ ┴ └───┘ ┴ └┘ ┴ └─────┘ └─────┘
src ┴ └───┘ ┴ └┘ ┴ └──┘└─────┘└──┘└─────┘┴ └───┘
typ ┴ ┴ └───┘ ┴ └┘ ┴ └──┘└─────┘└──┘└─────┘┴ └───┘
doc └──┘ └──┘ ┴ └───┘
txt └──┘ └──┘ ┴ └───┘
par └──┘ └──┘ ┴ └───┘
pid └┘ └──┘ ┴ ┴
st └──────────┘└─────────┘┴└─────┘
309 | -[1+ m] -[1+ n] := (pow_mul a (succ m) (succ n)).trans $
id └──┘ ┴┴ └──┘ ┴┴ └─────┘ ┴ └──┘ └──┘ └───┘
src └──┘ ┴ └──┘ ┴ └─────┘ └──┘ └──┘ └───┘
typ └──┘ ┴┴ └──┘ ┴┴ └─────┘ ┴ └──┘ └──┘ └───┘
310 show _ = (_⁻¹^_)⁻¹, by rw [inv_pow, inv_inv]
id ┴ └┘┴ └┘ └─────┘ └─────┘
src ┴ └┘┴ └┘ └──┘└─────┘└┘└─────┘└┘
typ ┴ └┘┴ └┘ └──┘└─────┘└┘└─────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └──────────┘└───────┘┴┴
311 theorem gsmul_mul' : ∀ (a : β) (m n : ℤ), m * n • a = n • (m • a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
312 @gpow_mul (multiplicative β) _
id └──────┘ └────────────┘ ┴
src └──────┘ └────────────┘
typ └──────┘ └────────────┘ ┴
313
314 theorem gpow_mul' (a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
315 by rw [mul_comm, gpow_mul]
id └──────┘ └──────┘
src └──┘└──────┘└┘└──────┘└┘
typ └──┘└──────┘└┘└──────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └───────────┘└────────┘┴┴
316 theorem gsmul_mul (a : β) (m n : ℤ) : m * n • a = m • (n • a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
317 by rw [mul_comm, gsmul_mul']
id └──────┘ └────────┘
src └──┘└──────┘└┘└────────┘└─
typ └──┘└──────┘└┘└────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────┘└──────────┘┴└
318
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
319 theorem gpow_bit0 (a : α) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n := gpow_add _ _ _
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
320 theorem bit0_gsmul (a : β) (n : ℤ) : bit0 n • a = n • a + n • a := gpow_add _ _ _
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──────┘
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
321
322 theorem gpow_bit1 (a : α) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
323 by rw [bit1, gpow_add]; simp [gpow_bit0]
id └──┘ └──────┘ └───────┘
src └──┘└──┘└┘└──────┘┴ └────┘└───────┘└┘
typ └──┘└──┘└┘└──────┘┴ └────┘└───────┘└┘
doc └──┘ └┘ ┴ └────┘ └┘
txt └──┘ └┘ ┴ └────┘ └┘
par └──┘ └┘ ┴ └────┘ └┘
pid └┘ └┘ ┴ ┴┴ ┴┴
st └───────┘└────────┘┴└─────────────────┘
324 theorem bit1_gsmul : ∀ (a : β) (n : ℤ), bit1 n • a = n • a + n • a + a :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
325 @gpow_bit1 (multiplicative β) _
id └───────┘ └────────────┘ ┴
src └───────┘ └────────────┘
typ └───────┘ └────────────┘ ┴
326
327 theorem gsmul_neg (a : β) (n : ℤ) : gsmul n (- a) = - gsmul n a :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ └───┘
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
328 begin
st └─────
329 induction n using int.induction_on with z ih z ih,
id ┴
src └────────┘ └────────────────────────────────────┘
typ └────────┘┴└────────────────────────────────────┘
doc └────────┘ └────────────────────────────────────┘
txt └────────┘ └────────────────────────────────────┘
par └────────┘ └────────────────────────────────────┘
pid ┴ └─────────────────────┘└─────────────┘
st ──────────────────────────────────────────────────┘└─
330 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
331 { rw [add_comm] {occs := occurrences.pos [1]}, simp [add_gsmul, ih, -add_comm] },
id └──────┘ └─────────────┘ ┴ ┴ └───────┘ └┘
src └──┘└──────┘└┘ └──────┘└─────────────┘┴┴┴┴┴ └────┘└───────┘└┘ └───────────┘
typ └──┘└──────┘└┘ └──────┘└─────────────┘┴┴┴┴┴ └────┘└───────┘└┘└┘└───────────┘
doc └──┘ └┘ └──────┘ ┴ ┴ ┴ └────┘ └┘ └───────────┘
txt └──┘ └┘ └──────┘ ┴ ┴ ┴ └────┘ └┘ └───────────┘
par └──┘ └┘ └──────┘ ┴ ┴ ┴ └────┘ └┘ └───────────┘
pid └┘ ┴┴ └──────┘ ┴ ┴ ┴ ┴┴ └┘ └──────────┘┴
st ───┘└──────────┘┴└────────────────────────────┘└────────────────────────────────┘└┘└
332 { rw [sub_eq_add_neg, add_comm] {occs := occurrences.pos [1]},
id └────────────┘ └──────┘ └─────────────┘ ┴ ┴
src └──┘└────────────┘└┘└──────┘└┘ └──────┘└─────────────┘┴┴┴┴┴
typ └──┘└────────────┘└┘└──────┘└┘ └──────┘└─────────────┘┴┴┴┴┴
doc └──┘ └┘ └┘ └──────┘ ┴ ┴ ┴
txt └──┘ └┘ └┘ └──────┘ ┴ ┴ ┴
par └──┘ └┘ └┘ └──────┘ ┴ ┴ ┴
pid └┘ └┘ ┴┴ └──────┘ ┴ ┴ ┴
st ─────────────────────┘└────────┘┴└────────────────────────────┘└─
333 simp [ih, add_gsmul, neg_gsmul, -add_comm] }
id └┘ └───────┘ └───────┘
src └────┘ └┘└───────┘└┘└───────┘└───────────┘
typ └────┘└┘└┘└───────┘└┘└───────┘└───────────┘
doc └────┘ └┘ └┘ └───────────┘
txt └────┘ └┘ └┘ └───────────┘
par └────┘ └┘ └┘ └───────────┘
pid ┴┴ └┘ └┘ └──────────┘┴
st ──────────────────────────────────────────────┘└─
334 end
st ──┘
335
336 end group
337
338 namespace is_group_hom
339 variables {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f]
id └───┘ └───┘ └──────────┘
src └───┘ └───┘ └──────────┘
typ └───┘ └───┘ └──────────┘
doc └──────────┘
340
341 theorem map_pow (a : α) (n : ℕ) : f (a ^ n) = f a ^ n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
342 is_monoid_hom.map_pow f a n
id └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴
343
344 theorem map_gpow (a : α) (n : ℤ) : f (a ^ n) = f a ^ n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
345 by cases n; [exact is_group_hom.map_pow f _ _,
id ┴ ┴ └──────────────────┘ ┴
src └────┘ ┴└────┘└──────────────────┘┴ └──┘
typ └────┘┴ ┴└────┘└──────────────────┘┴┴└──┘
doc └────┘ └────┘ ┴ └──┘
txt └────┘ └────┘ ┴ └──┘
par └────┘ └────┘ ┴ └──┘
pid ┴ ┴ ┴ └──┘
st └────────────────────────────────────────────
346 exact (is_group_hom.map_inv f _).trans (congr_arg _ $ is_group_hom.map_pow f _ _)]
id └──────────────────┘ └───────┘ └──────────────────┘ ┴
src └────┘ └──────────────────┘┴ └────────┘ └───────┘└─┘ ┴└──────────────────┘┴ └───┘
typ └────┘ └──────────────────┘┴ └────────┘ └───────┘└─┘ ┴└──────────────────┘┴┴└───┘
doc └────┘ └──────────────────┘┴ └────────┘ └─┘ ┴ ┴ └───┘
txt └────┘ ┴ └────────┘ └─┘ ┴ ┴ └───┘
par └────┘ ┴ └────────┘ └─┘ ┴ ┴ └───┘
pid ┴ ┴ └────────┘ └─┘ ┴ ┴ └───┘
st ───────────────────────────────────────────────────────────────────────────────────┘
347
348 end is_group_hom
349
350 namespace is_add_group_hom
351 variables {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f]
id └───────┘ └───────┘ └──────────────┘
src └───────┘ └───────┘ └──────────────┘
typ └───────┘ └───────┘ └──────────────┘
doc └──────────────┘
352
353 theorem map_smul (a : α) (n : ℕ) : f (n • a) = n • f a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
354 is_add_monoid_hom.map_smul f a n
id └────────────────────────┘ ┴ ┴ ┴
src └────────────────────────┘
typ └────────────────────────┘ ┴ ┴ ┴
355
356 theorem map_gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src ┴ └───┘ ┴ └───┘
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
357 @is_group_hom.map_gpow (multiplicative α) (multiplicative β) _ _ f _ a n
id └───────────────────┘ └────────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
src └───────────────────┘ └────────────┘ └────────────┘
typ └───────────────────┘ └────────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
358
359 end is_add_group_hom
360
361 namespace monoid_hom
362 variables {β : Type v} [group α] [group β] (f : α →* β)
id └───┘ └───┘ └┘
src └───┘ └───┘ └┘
typ └───┘ └───┘ └┘
doc └┘
363
364 @[simp] theorem map_gpow (a : α) (n : ℤ) : f (a ^ n) = f a ^ n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
365 by cases n; [exact f.map_pow _ _,
id ┴ ┴ └───────┘
src └────┘ ┴└────┘└───────┘└──┘
typ └────┘┴ ┴└────┘└───────┘└──┘
doc └────┘ └────┘ └──┘
txt └────┘ └────┘ └──┘
par └────┘ └────┘ └──┘
pid ┴ ┴ └──┘
st └───────────────────────────────
366 exact (f.map_inv _).trans (congr_arg _ $ f.map_pow _ _)]
id └───────┘ └───────┘ └───────┘
src └────┘ └───────┘└────────┘ └───────┘└─┘ ┴└───────┘└───┘
typ └────┘ └───────┘└────────┘ └───────┘└─┘ ┴└───────┘└───┘
doc └────┘ └───────┘└────────┘ └─┘ ┴ └───┘
txt └────┘ └────────┘ └─┘ ┴ └───┘
par └────┘ └────────┘ └─┘ ┴ └───┘
pid ┴ └────────┘ └─┘ ┴ └───┘
st ─────────────────────────────────────────────────────────┘
367
368 end monoid_hom
369
370 namespace add_monoid_hom
371 variables {β : Type v} [add_group α] [add_group β] (f : α →+ β)
id └───────┘ └───────┘ └┘
src └───────┘ └───────┘ └┘
typ └───────┘ └───────┘ └┘
doc └┘
372
373 @[simp] theorem map_gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src ┴ └───┘ ┴ └───┘
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └──┘
374 by cases n; [exact f.map_smul _ _,
id ┴ ┴ └────────┘
src └────┘ ┴└────┘└────────┘└──┘
typ └────┘┴ ┴└────┘└────────┘└──┘
doc └────┘ └────┘ └──┘
txt └────┘ └────┘ └──┘
par └────┘ └────┘ └──┘
pid ┴ ┴ └──┘
st └────────────────────────────────
375 exact (f.map_neg _).trans (congr_arg _ $ f.map_smul _ _)]
id └───────┘ └───────┘ └────────┘
src └────┘ └───────┘└────────┘ └───────┘└─┘ ┴└────────┘└───┘
typ └────┘ └───────┘└────────┘ └───────┘└─┘ ┴└────────┘└───┘
doc └────┘ └────────┘ └─┘ ┴ └───┘
txt └────┘ └────────┘ └─┘ ┴ └───┘
par └────┘ └────────┘ └─┘ ┴ └───┘
pid ┴ └────────┘ └─┘ ┴ └───┘
st ──────────────────────────────────────────────────────────┘
376
377 end add_monoid_hom
378 local infix ` •ℤ `:70 := gsmul
id └───┘
src └───┘
typ └───┘
379 open_locale smul
380
381 section comm_monoid
382 variables [comm_group α] {β : Type*} [add_comm_group β]
id └────────┘ └────────────┘
src └────────┘ └────────────┘
typ └────────┘ └────────────┘
383
384 theorem mul_gpow (a b : α) : ∀ n:ℤ, (a * b)^n = a^n * b^n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
385 | (n : ℕ) := mul_pow a b n
id ┴ ┴ └─────┘ ┴ ┴
src ┴ └─────┘
typ ┴ ┴ └─────┘ ┴ ┴
386 | -[1+ n] := show _⁻¹=_⁻¹*_⁻¹, by rw [mul_pow, mul_inv_rev, mul_comm]
id └──┘ ┴ └┘┴ └┘┴ └┘ └─────┘ └─────────┘ └──────┘
src └──┘ ┴ └┘┴ └┘┴ └┘ └──┘└─────┘└┘└─────────┘└┘└──────┘└┘
typ └──┘ ┴ └┘┴ └┘┴ └┘ └──┘└─────┘└┘└─────────┘└┘└──────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st └──────────┘└───────────┘└────────┘┴┴
387 theorem gsmul_add : ∀ (a b : β) (n : ℤ), n •ℤ (a + b) = n •ℤ a + n •ℤ b :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
src ┴ └┘ ┴ ┴ └┘ ┴ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
388 @mul_gpow (multiplicative β) _
id └──────┘ └────────────┘ ┴
src └──────┘ └────────────┘
typ └──────┘ └────────────┘ ┴
389
390 theorem gsmul_sub : ∀ (a b : β) (n : ℤ), gsmul n (a - b) = gsmul n a - gsmul n b :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
391 by simp [gsmul_add, gsmul_neg]
id └───────┘ └───────┘
src └────┘└───────┘└┘└───────┘└─
typ └────┘└───────┘└┘└───────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────
392
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
393 instance gpow.is_group_hom (n : ℤ) : is_group_hom ((^ n) : α → α) :=
id ┴ └──────────┘ ┴ ┴ ┴ ┴
src ┴ └──────────┘ ┴
typ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc └──────────┘
394 { map_mul := λ _ _, mul_gpow _ _ n }
id ┴ ┴ └──────┘ ┴
src └──────┘
typ ┴ ┴ └──────┘ ┴
395
396 instance gsmul.is_add_group_hom (n : ℤ) : is_add_group_hom (gsmul n : β → β) :=
id ┴ └──────────────┘ └───┘ ┴ ┴ ┴
src ┴ └──────────────┘ └───┘
typ ┴ └──────────────┘ └───┘ ┴ ┴ ┴
doc └──────────────┘
397 { map_add := λ _ _, gsmul_add _ _ n }
id ┴ ┴ └───────┘ ┴
src └───────┘
typ ┴ ┴ └───────┘ ┴
398
399 end comm_monoid
400
401 section group
402
403 @[instance]
404 theorem is_add_group_hom.gsmul
405 {α β} [add_group α] [add_comm_group β] (f : α → β) [is_add_group_hom f] (z : ℤ) :
id └───────┘ ┴ └────────────┘ ┴ ┴ ┴ └──────────────┘ ┴ ┴
src └───────┘ └────────────┘ └──────────────┘ ┴
typ └───────┘ ┴ └────────────┘ ┴ ┴ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘
406 is_add_group_hom (λa, gsmul z (f a)) :=
id └──────────────┘ ┴ └───┘ ┴ ┴ ┴
src └──────────────┘ └───┘
typ └──────────────┘ ┴ └───┘ ┴ ┴ ┴
doc └──────────────┘
407 { map_add := assume a b, by rw [is_add_hom.map_add f, gsmul_add] }
id ┴ ┴ └────────────────┘ ┴ └───────┘
src └──┘└────────────────┘┴ └┘└───────┘└┘
typ ┴ ┴ └──┘└────────────────┘┴┴└┘└───────┘└┘
doc └──┘ ┴ └┘ └┘
txt └──┘ ┴ └┘ └┘
par └──┘ ┴ └┘ └┘
pid └┘ ┴ └┘ ┴┴
st └───────────────────────┘└─────────┘┴┴
408
409 end group
410
411 @[simp] lemma with_bot.coe_smul [add_monoid α] (a : α) (n : ℕ) :
id └────────┘ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴ ┴
doc └──┘
412 ((add_monoid.smul n a : α) : with_bot α) = add_monoid.smul n a :=
id └─────────────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ └──────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────────────┘ ┴ ┴
413 by induction n; simp [*, succ_smul]; refl
id ┴ └───────┘
src └────────┘ └───────┘└───────┘┴ └────
typ └────────┘┴ └───────┘└───────┘┴ └────
doc └────────┘ └───────┘ ┴ └────
txt └────────┘ └───────┘ ┴ └────
par └────────┘ └───────┘ ┴ └────
pid ┴ ┴└──┘ ┴ └
st └───────────────────────────────────────
414
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
415 theorem add_monoid.smul_eq_mul' [semiring α] (a : α) (n : ℕ) : n • a = a * n :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
416 by induction n with n ih; [rw [add_monoid.zero_smul, nat.cast_zero, mul_zero],
id ┴ ┴ └──────────────────┘ └───────────┘ └──────┘
src └────────┘ └────────┘ ┴└──┘└──────────────────┘└┘└───────────┘└┘└──────┘┴
typ └────────┘┴└────────┘ ┴└──┘└──────────────────┘└┘└───────────┘└┘└──────┘┴
doc └────────┘ └────────┘ └──┘ └┘ └┘ ┴
txt └────────┘ └────────┘ └──┘ └┘ └┘ ┴
par └────────┘ └────────┘ └──┘ └┘ └┘ ┴
pid ┴ ┴└───────┘ └┘ └┘ └┘ ┴
st └───────────────────────────┘└──────────────────┘└─────────────┘└────────┘┴└─
417 rw [succ_smul', ih, nat.cast_succ, mul_add, mul_one]]
id └────────┘ └┘ └───────────┘ └─────┘ └─────┘
src └──┘└────────┘└┘ └┘└───────────┘└┘└─────┘└┘└─────┘┴
typ └──┘└────────┘└┘└┘└┘└───────────┘└┘└─────┘└┘└─────┘┴
doc └──┘ └┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴
st ─────┘└────────┘└──┘└─────────────┘└───────┘└───────┘┴┴
418
419 theorem add_monoid.smul_eq_mul [semiring α] (n : ℕ) (a : α) : n • a = n * a :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
420 by rw [add_monoid.smul_eq_mul', nat.mul_cast_comm]
id └─────────────────────┘ └───────────────┘
src └──┘└─────────────────────┘└┘└───────────────┘└─
typ └──┘└─────────────────────┘└┘└───────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────────────────────┘└─────────────────┘┴└
421
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
422 theorem add_monoid.mul_smul_left [semiring α] (a b : α) (n : ℕ) : n • (a * b) = a * (n • b) :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
423 by rw [add_monoid.smul_eq_mul', add_monoid.smul_eq_mul', mul_assoc]
id └─────────────────────┘ └─────────────────────┘ └───────┘
src └──┘└─────────────────────┘└┘└─────────────────────┘└┘└───────┘└─
typ └──┘└─────────────────────┘└┘└─────────────────────┘└┘└───────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └──────────────────────────┘└───────────────────────┘└─────────┘┴└
424
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
425 theorem add_monoid.mul_smul_assoc [semiring α] (a b : α) (n : ℕ) : n • (a * b) = n • a * b :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
426 by rw [add_monoid.smul_eq_mul, add_monoid.smul_eq_mul, mul_assoc]
id └────────────────────┘ └────────────────────┘ └───────┘
src └──┘└────────────────────┘└┘└────────────────────┘└┘└───────┘└─
typ └──┘└────────────────────┘└┘└────────────────────┘└┘└───────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └─────────────────────────┘└──────────────────────┘└─────────┘┴└
427
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
428 lemma zero_pow [semiring α] : ∀ {n : ℕ}, 0 < n → (0 : α) ^ n = 0
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
429 | (n+1) _ := zero_mul _
id ┴ └──────┘
src ┴ └──────┘
typ ┴ └──────┘
430
431 @[simp, move_cast] theorem nat.cast_pow [semiring α] (n m : ℕ) : (↑(n ^ m) : α) = ↑n ^ m :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └──┘ └───────┘
432 by induction m with m ih; [exact nat.cast_one, rw [nat.pow_succ, pow_succ', nat.cast_mul, ih]]
id ┴ ┴ └──────────┘ └──────────┘ └───────┘ └──────────┘ └┘
src └────────┘ └────────┘ ┴└────┘└──────────┘ └──┘└──────────┘└┘└───────┘└┘└──────────┘└┘ ┴
typ └────────┘┴└────────┘ ┴└────┘└──────────┘ └──┘└──────────┘└┘└───────┘└┘└──────────┘└┘└┘┴
doc └────────┘ └────────┘ └────┘ └──┘ └┘ └┘ └┘ ┴
txt └────────┘ └────────┘ └────┘ └──┘ └┘ └┘ └┘ ┴
par └────────┘ └────────┘ └────┘ └──┘ └┘ └┘ └┘ ┴
pid ┴ ┴└───────┘ ┴ └┘ └┘ └┘ └┘ ┴
st └───────────────────────────────────────────────┘└──────────┘└─────────┘└────────────┘└──┘┴┴
433
434 @[simp, move_cast] theorem int.coe_nat_pow (n m : ℕ) : ((n ^ m : ℕ) : ℤ) = n ^ m :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───────┘
435 by induction m with m ih; [exact int.coe_nat_one, rw [nat.pow_succ, pow_succ', int.coe_nat_mul, ih]]
id ┴ ┴ └─────────────┘ └──────────┘ └───────┘ └─────────────┘ └┘
src └────────┘ └────────┘ ┴└────┘└─────────────┘ └──┘└──────────┘└┘└───────┘└┘└─────────────┘└┘ ┴
typ └────────┘┴└────────┘ ┴└────┘└─────────────┘ └──┘└──────────┘└┘└───────┘└┘└─────────────┘└┘└┘┴
doc └────────┘ └────────┘ └────┘ └──┘ └┘ └┘ └┘ ┴
txt └────────┘ └────────┘ └────┘ └──┘ └┘ └┘ └┘ ┴
par └────────┘ └────────┘ └────┘ └──┘ └┘ └┘ └┘ ┴
pid ┴ ┴└───────┘ ┴ └┘ └┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────┘└──────────┘└─────────┘└───────────────┘└──┘┴┴
436
437 theorem int.nat_abs_pow (n : ℤ) (k : ℕ) : int.nat_abs (n ^ k) = (int.nat_abs n) ^ k :=
id ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
src ┴ ┴ └─────────┘ ┴ ┴ └─────────┘ ┴
typ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
438 by induction k with k ih; [refl, rw [pow_succ', int.nat_abs_mul, nat.pow_succ, ih]]
id ┴ ┴ └───────┘ └─────────────┘ └──────────┘ └┘
src └────────┘ └────────┘ ┴└──┘ └──┘└───────┘└┘└─────────────┘└┘└──────────┘└┘ ┴
typ └────────┘┴└────────┘ ┴└──┘ └──┘└───────┘└┘└─────────────┘└┘└──────────┘└┘└┘┴
doc └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ └┘ ┴
txt └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ └┘ ┴
par └────────┘ └────────┘ └──┘ └──┘ └┘ └┘ └┘ ┴
pid ┴ ┴└───────┘ └┘ └┘ └┘ └┘ ┴
st └─────────────────────────────────┘└───────┘└───────────────┘└────────────┘└──┘┴┴
439
440 theorem is_semiring_hom.map_pow {β} [semiring α] [semiring β]
id └──────┘ ┴ └──────┘ ┴
src └──────┘ └──────┘
typ └──────┘ ┴ └──────┘ ┴
441 (f : α → β) [is_semiring_hom f] (x : α) (n : ℕ) : f (x ^ n) = f x ^ n :=
id ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
442 by induction n with n ih; [exact is_semiring_hom.map_one f,
id ┴ ┴ └─────────────────────┘ ┴
src └────────┘ └────────┘ ┴└────┘└─────────────────────┘┴
typ └────────┘┴└────────┘ ┴└────┘└─────────────────────┘┴┴
doc └────────┘ └────────┘ └────┘ ┴
txt └────────┘ └────────┘ └────┘ ┴
par └────────┘ └────────┘ └────┘ ┴
pid ┴ ┴└───────┘ ┴ ┴
st └─────────────────────────────────────────────────────────
443 rw [pow_succ, pow_succ, is_semiring_hom.map_mul f, ih]]
id └──────┘ └──────┘ └─────────────────────┘ ┴ └┘
src └──┘└──────┘└┘└──────┘└┘└─────────────────────┘┴ └┘ ┴
typ └──┘└──────┘└┘└──────┘└┘└─────────────────────┘┴┴└┘└┘┴
doc └──┘ └┘ └┘ ┴ └┘ ┴
txt └──┘ └┘ └┘ ┴ └┘ ┴
par └──┘ └┘ └┘ ┴ └┘ ┴
pid └┘ └┘ └┘ ┴ └┘ ┴
st ─────┘└──────┘└────────┘└─────────────────────────┘└──┘┴┴
444
445 @[simp] lemma ring_hom.map_pow {β} [semiring α] [semiring β] (f : α →+* β) (a) :
id └──────┘ ┴ └──────┘ ┴ ┴ └─┘ ┴
src └──────┘ └──────┘ └─┘
typ └──────┘ ┴ └──────┘ ┴ ┴ └─┘ ┴
doc └──┘ └─┘
446 ∀ n : ℕ, f (a ^ n) = (f a) ^ n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
447 monoid_hom.map_pow f.to_monoid_hom a
id └────────────────┘ ┴└────────────┘ ┴
src └────────────────┘ └────────────┘
typ └────────────────┘ ┴└────────────┘ ┴
448
449 theorem neg_one_pow_eq_or {R} [ring R] : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n = -1
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
450 | 0 := or.inl rfl
id └────┘ └─┘
src └────┘ └─┘
typ └────┘ └─┘
451 | (n+1) := (neg_one_pow_eq_or n).swap.imp
id ┴┴ └───────────────┘ └──┘ └─┘
src ┴ └──┘ └─┘
typ ┴┴ └───────────────┘ └──┘ └─┘
452 (λ h, by rw [pow_succ, h, neg_one_mul, neg_neg])
id ┴ └──────┘ ┴ └─────────┘ └─────┘
src └──┘└──────┘└┘ └┘└─────────┘└┘└─────┘┴
typ ┴ └──┘└──────┘└┘┴└┘└─────────┘└┘└─────┘┴
doc └──┘ └┘ └┘└─────────┘└┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └───────────┘└─┘└───────────┘└───────┘┴
453 (λ h, by rw [pow_succ, h, mul_one])
id ┴ └──────┘ ┴ └─────┘
src └──┘└──────┘└┘ └┘└─────┘┴
typ ┴ └──┘└──────┘└┘┴└┘└─────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └───────────┘└─┘└───────┘┴
454
455 lemma pow_dvd_pow [comm_semiring α] (a : α) {m n : ℕ} (h : m ≤ n) :
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
456 a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_sub_cancel' h]⟩
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └─────────────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └────┘└─────┘└┘└─────────────────┘┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└─────┘└┘└─────────────────┘┴┴┴
doc └────┘ └┘ ┴ ┴
txt └────┘ └┘ ┴ ┴
par └────┘ └┘ ┴ ┴
pid └──┘ └┘ ┴ ┴
st └────────────┘└─────────────────────┘┴
457
458 theorem gsmul_eq_mul [ring α] (a : α) : ∀ n, n •ℤ a = n * a
id └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └──┘ └┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
459 | (n : ℕ) := add_monoid.smul_eq_mul _ _
id ┴ └────────────────────┘
src ┴ └────────────────────┘
typ ┴ └────────────────────┘
460 | -[1+ n] := show -(_•_)=-_*_, by rw [neg_mul_eq_neg_mul_symm, add_monoid.smul_eq_mul, nat.cast_succ]
id └──┘ ┴ ┴ ┴ ┴┴ ┴ └─────────────────────┘ └────────────────────┘ └───────────┘
src └──┘ ┴ ┴ ┴ ┴┴ ┴ └──┘└─────────────────────┘└┘└────────────────────┘└┘└───────────┘└─
typ └──┘ ┴ ┴ ┴ ┴┴ ┴ └──┘└─────────────────────┘└┘└────────────────────┘└┘└───────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └──────────────────────────┘└──────────────────────┘└─────────────┘┴└
461
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
462 theorem gsmul_eq_mul' [ring α] (a : α) (n : ℤ) : n •ℤ a = a * n :=
id └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ └┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
463 by rw [gsmul_eq_mul, int.mul_cast_comm]
id └──────────┘ └───────────────┘
src └──┘└──────────┘└┘└───────────────┘└─
typ └──┘└──────────┘└┘└───────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────────┘└─────────────────┘┴└
464
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
465 theorem mul_gsmul_left [ring α] (a b : α) (n : ℤ) : n •ℤ (a * b) = a * (n •ℤ b) :=
id └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └──┘ ┴ └┘ ┴ ┴ ┴ └┘
typ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
466 by rw [gsmul_eq_mul', gsmul_eq_mul', mul_assoc]
id └───────────┘ └───────────┘ └───────┘
src └──┘└───────────┘└┘└───────────┘└┘└───────┘└─
typ └──┘└───────────┘└┘└───────────┘└┘└───────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └────────────────┘└─────────────┘└─────────┘┴└
467
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
468 theorem mul_gsmul_assoc [ring α] (a b : α) (n : ℤ) : n •ℤ (a * b) = n •ℤ a * b :=
id └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴ └┘ ┴ ┴ └┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
469 by rw [gsmul_eq_mul, gsmul_eq_mul, mul_assoc]
id └──────────┘ └──────────┘ └───────┘
src └──┘└──────────┘└┘└──────────┘└┘└───────┘└─
typ └──┘└──────────┘└┘└──────────┘└┘└───────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └───────────────┘└────────────┘└─────────┘┴└
470
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
471 @[simp, move_cast] theorem int.cast_pow [ring α] (n : ℤ) (m : ℕ) : (↑(n ^ m) : α) = ↑n ^ m :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └──┘ └───────┘
472 by induction m with m ih; [exact int.cast_one,
id ┴ ┴ └──────────┘
src └────────┘ └────────┘ ┴└────┘└──────────┘
typ └────────┘┴└────────┘ ┴└────┘└──────────┘
doc └────────┘ └────────┘ └────┘
txt └────────┘ └────────┘ └────┘
par └────────┘ └────────┘ └────┘
pid ┴ ┴└───────┘ ┴
st └────────────────────────────────────────────
473 rw [pow_succ, pow_succ, int.cast_mul, ih]]
id └──────┘ └──────┘ └──────────┘ └┘
src └──┘└──────┘└┘└──────┘└┘└──────────┘└┘ ┴
typ └──┘└──────┘└┘└──────┘└┘└──────────┘└┘└┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ─────┘└──────┘└────────┘└────────────┘└──┘┴┴
474
475 lemma neg_one_pow_eq_pow_mod_two [ring α] {n : ℕ} : (-1 : α) ^ n = -1 ^ (n % 2) :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
476 by rw [← nat.mod_add_div n 2, pow_add, pow_mul]; simp [pow_two]
id └─────────────┘ ┴ └─────┘ └─────┘ └─────┘
src └────┘└─────────────┘┴ └──┘└─────┘└┘└─────┘┴ └────┘└─────┘└─
typ └────┘└─────────────┘┴┴└──┘└─────┘└┘└─────┘┴ └────┘└─────┘└─
doc └────┘ ┴ └──┘ └┘ ┴ └────┘ └─
txt └────┘ ┴ └──┘ └┘ ┴ └────┘ └─
par └────┘ ┴ └──┘ └┘ ┴ └────┘ └─
pid └──┘ ┴ └──┘ └┘ ┴ ┴┴ ┴└
st └───────────────────────┘└────────┘└───────┘┴└────────────────
477
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
478 theorem sq_sub_sq [comm_ring α] (a b : α) : a ^ 2 - b ^ 2 = (a + b) * (a - b) :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
479 by rw [pow_two, pow_two, mul_self_sub_mul_self]
id └─────┘ └─────┘ └───────────────────┘
src └──┘└─────┘└┘└─────┘└┘└───────────────────┘└─
typ └──┘└─────┘└┘└─────┘└┘└───────────────────┘└─
doc └──┘ └┘ └┘└───────────────────┘└─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └──────────┘└───────┘└─────────────────────┘┴└
480
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
481 theorem pow_eq_zero [domain α] {x : α} {n : ℕ} (H : x^n = 0) : x = 0 :=
id └────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc └────┘
482 begin
st └─────
483 induction n with n ih,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─
484 { rw pow_zero at H,
id └──────┘
src └─┘└──────┘└───┘
typ └─┘└──────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───┘└──────────────┘└─
485 rw [← mul_one x, H, mul_zero] },
id └─────┘ ┴ ┴ └──────┘
src └────┘└─────┘┴ └┘ └┘└──────┘└┘
typ └────┘└─────┘┴┴└┘┴└┘└──────┘└┘
doc └────┘ ┴ └┘ └┘ └┘
txt └────┘ ┴ └┘ └┘ └┘
par └────┘ ┴ └┘ └┘ └┘
pid └──┘ ┴ └┘ └┘ ┴┴
st ──────────────────┘└─┘└────────┘┴┴└┘└
486 exact or.cases_on (mul_eq_zero.1 H) id ih
id └─────────┘ └─────────┘ ┴ └┘ └┘
src └────┘└─────────┘┴ └─────────┘└─┘ └┘└┘┴ ┴
typ └────┘└─────────┘┴ └─────────┘└─┘┴└┘└┘┴└┘┴
doc └────┘ ┴ └─────────┘└─┘ └┘ ┴ ┴
txt └────┘ ┴ └─┘ └┘ ┴ ┴
par └────┘ ┴ └─┘ └┘ ┴ ┴
pid ┴ ┴ └─┘ └┘ ┴ ┴
st ───────────────────────────────────────────┘
487 end
st └─┘
488
489 @[field_simps] theorem pow_ne_zero [domain α] {a : α} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ └────┘
490 mt pow_eq_zero h
id └┘ └─────────┘ ┴
src └┘ └─────────┘
typ └┘ └─────────┘ ┴
491
492 @[simp] theorem one_div_pow [division_ring α] {a : α} (ha : a ≠ 0) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n :=
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
493 by induction n with n ih; [exact (div_one _).symm,
id ┴ ┴ └─────┘
src └────────┘ └────────┘ ┴└────┘ └─────┘└──────┘
typ └────────┘┴└────────┘ ┴└────┘ └─────┘└──────┘
doc └────────┘ └────────┘ └────┘ └──────┘
txt └────────┘ └────────┘ └────┘ └──────┘
par └────────┘ └────────┘ └────┘ └──────┘
pid ┴ ┴└───────┘ ┴ └─────┘┴
st └────────────────────────────────────────────────
494 rw [pow_succ', ih, division_ring.one_div_mul_one_div (pow_ne_zero _ ha) ha]]; refl
id └───────┘ └┘ └───────────────────────────────┘ └─────────┘ └┘
src └──┘└───────┘└┘ └┘└───────────────────────────────┘┴ └─────────┘└─┘ └┘ ┴ └────
typ └──┘└───────┘└┘└┘└┘└───────────────────────────────┘┴ └─────────┘└─┘ └┘└┘┴ └────
doc └──┘ └┘ └┘ ┴ └─┘ └┘ ┴ └────
txt └──┘ └┘ └┘ ┴ └─┘ └┘ ┴ └────
par └──┘ └┘ └┘ ┴ └─┘ └┘ ┴ └────
pid └┘ └┘ └┘ ┴ └─┘ └┘ ┴ └
st ─────┘└───────┘└──┘└───────────────────────────────────────────────────────┘┴└───────
495
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
496 @[simp] theorem division_ring.inv_pow [division_ring α] {a : α} (ha : a ≠ 0) (n : ℕ) : a⁻¹ ^ n = (a ^ n)⁻¹ :=
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └───────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
doc └──┘
497 by simpa only [inv_eq_one_div] using one_div_pow ha n
id └────────────┘ └─────────┘ └┘ ┴
src └──────────┘└────────────┘└──────┘└─────────┘┴ ┴ └
typ └──────────┘└────────────┘└──────┘└─────────┘┴└┘┴┴└
doc └──────────┘ └──────┘ ┴ ┴ └
txt └──────────┘ └──────┘ ┴ ┴ └
par └──────────┘ └──────┘ ┴ ┴ └
pid ┴└──┘└┘ ┴┴└────┘ ┴ ┴ └
st └───────────────────────────────────────────────────
498
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
499 @[simp] theorem div_pow [field α] (a : α) {b : α} (hb : b ≠ 0) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
500 by rw [div_eq_mul_one_div, mul_pow, one_div_pow hb, ← div_eq_mul_one_div]
id └────────────────┘ └─────┘ └─────────┘ └┘ └────────────────┘
src └──┘└────────────────┘└┘└─────┘└┘└─────────┘┴ └──┘└────────────────┘└─
typ └──┘└────────────────┘└┘└─────┘└┘└─────────┘┴└┘└──┘└────────────────┘└─
doc └──┘ └┘ └┘ ┴ └──┘ └─
txt └──┘ └┘ └┘ ┴ └──┘ └─
par └──┘ └┘ └┘ ┴ └──┘ └─
pid └┘ └┘ └┘ ┴ └──┘ ┴└
st └─────────────────────┘└───────┘└──────────────┘└────────────────────┘┴└
501
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
502 theorem add_monoid.smul_nonneg [ordered_comm_monoid α] {a : α} (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ n • a
id └─────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ ┴ ┴ ┴ ┴
typ └─────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────────┘
503 | 0 := le_refl _
id └─────┘
src └─────┘
typ └─────┘
504 | (n+1) := add_nonneg' H (add_monoid.smul_nonneg n)
id ┴┴ └─────────┘ ┴ └────────────────────┘
src ┴ └─────────┘
typ ┴┴ └─────────┘ ┴ └────────────────────┘
505
506 lemma pow_abs [decidable_linear_ordered_comm_ring α] (a : α) (n : ℕ) : (abs a)^n = abs (a^n) :=
id └────────────────────────────────┘ ┴ ┴ ┴ └─┘ ┴ ┴┴ ┴ └─┘ ┴┴┴
src └────────────────────────────────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
typ └────────────────────────────────┘ ┴ ┴ ┴ └─┘ ┴ ┴┴ ┴ └─┘ ┴┴┴
507 by induction n with n ih; [exact (abs_one).symm,
id ┴ ┴ └─────┘
src └────────┘ └────────┘ ┴└────┘ └─────┘└────┘
typ └────────┘┴└────────┘ ┴└────┘ └─────┘└────┘
doc └────────┘ └────────┘ └────┘ └────┘
txt └────────┘ └────────┘ └────┘ └────┘
par └────────┘ └────────┘ └────┘ └────┘
pid ┴ ┴└───────┘ ┴ └───┘┴
st └──────────────────────────────────────────────
508 rw [pow_succ, pow_succ, ih, abs_mul]]
id └──────┘ └──────┘ └┘ └─────┘
src └──┘└──────┘└┘└──────┘└┘ └┘└─────┘┴
typ └──┘└──────┘└┘└──────┘└┘└┘└┘└─────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ─────┘└──────┘└────────┘└──┘└───────┘┴┴
509
510 lemma abs_neg_one_pow [decidable_linear_ordered_comm_ring α] (n : ℕ) : abs ((-1 : α)^n) = 1 :=
id └────────────────────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴
src └────────────────────────────────┘ ┴ └─┘ ┴ ┴ ┴
typ └────────────────────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴
511 by rw [←pow_abs, abs_neg, abs_one, one_pow]
id └─────┘ └─────┘ └─────┘ └─────┘
src └───┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└─
typ └───┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└─
doc └───┘ └┘ └┘ └┘ └─
txt └───┘ └┘ └┘ └┘ └─
par └───┘ └┘ └┘ └┘ └─
pid └─┘ └┘ └┘ └┘ ┴└
st └───────────┘└───────┘└───────┘└───────┘┴└
512
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
513 @[field_simps] lemma inv_pow' [discrete_field α] (a : α) (n : ℕ) : a⁻¹ ^ n = (a ^ n)⁻¹ :=
id └────────────┘ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └────────────┘ ┴ └┘ ┴ ┴ ┴ └┘
typ └────────────┘ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
doc └─────────┘
514 by induction n; simp [*, pow_succ, mul_inv', mul_comm]
id ┴ └──────┘ └──────┘ └──────┘
src └────────┘ └───────┘└──────┘└┘└──────┘└┘└──────┘└─
typ └────────┘┴ └───────┘└──────┘└┘└──────┘└┘└──────┘└─
doc └────────┘ └───────┘ └┘ └┘ └─
txt └────────┘ └───────┘ └┘ └┘ └─
par └────────┘ └───────┘ └┘ └┘ └─
pid ┴ ┴└──┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────
515
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
516 @[field_simps] lemma pow_div [discrete_field α] (a b : α) (n : ℕ) : (a / b)^n = a^n / b^n :=
id └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
doc └─────────┘
517 by simp [div_eq_mul_inv, mul_pow, inv_pow']
id └────────────┘ └─────┘ └──────┘
src └────┘└────────────┘└┘└─────┘└┘└──────┘└─
typ └────┘└────────────┘└┘└─────┘└┘└──────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └─────────────────────────────────────────
518
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
519 lemma pow_inv [division_ring α] (a : α) : ∀ n : ℕ, a ≠ 0 → (a^n)⁻¹ = (a⁻¹)^n
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴└┘ ┴┴
src └───────────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴└┘ ┴┴
520 | 0 ha := inv_one
id └─────┘
src └─────┘
typ └─────┘
521 | (n+1) ha := by rw [pow_succ, pow_succ', mul_inv_eq (pow_ne_zero _ ha) ha, pow_inv _ ha]
id ┴ └──────┘ └───────┘ └────────┘ └─────────┘ └┘ └─────┘ └┘
src ┴ └──┘└──────┘└┘└───────┘└┘└────────┘┴ └─────────┘└─┘ └┘ └┘ └─┘ └─
typ ┴ └──┘└──────┘└┘└───────┘└┘└────────┘┴ └─────────┘└─┘ └┘└┘└┘└─────┘└─┘└┘└─
doc └──┘ └┘ └┘ ┴ └─┘ └┘ └┘ └─┘ └─
txt └──┘ └┘ └┘ ┴ └─┘ └┘ └┘ └─┘ └─
par └──┘ └┘ └┘ ┴ └─┘ └┘ └┘ └─┘ └─
pid └┘ └┘ └┘ ┴ └─┘ └┘ └┘ └─┘ ┴└
st └───────────┘└─────────┘└────────────────────────────────┘└────────────┘┴└
522
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
523 namespace add_monoid
524 variable [ordered_comm_monoid α]
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
525
526 theorem smul_le_smul {a : α} {n m : ℕ} (ha : 0 ≤ a) (h : n ≤ m) : n • a ≤ m • a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
527 let ⟨k, hk⟩ := nat.le.dest h in
id └─┘ ┴ └─────────┘ ┴
src └─────────┘
typ └─┘ ┴ └─────────┘ ┴
528 calc n • a = n • a + 0 : (add_zero _).symm
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └──┘
src ┴ ┴ ┴ └──────┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └──┘
529 ... ≤ n • a + k • a : add_le_add_left' (smul_nonneg ha _)
id ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘ └─────────┘ └┘
src ┴ ┴ ┴ └──────────────┘ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘ └─────────┘ └┘
530 ... = m • a : by rw [← hk, add_smul]
id ┴ ┴ ┴ └┘ └──────┘
src ┴ └────┘ └┘└──────┘└─
typ ┴ ┴ ┴ └────┘└┘└┘└──────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ ┴└
st └───────┘└────────┘┴└
531
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
532 lemma smul_le_smul_of_le_right {a b : α} (hab : a ≤ b) : ∀ i : ℕ, i • a ≤ i • b
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
533 | 0 := by simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
534 | (k+1) := add_le_add' hab (smul_le_smul_of_le_right _)
id ┴ └─────────┘ └─┘ └──────────────────────┘
src ┴ └─────────┘
typ ┴ └─────────┘ └─┘ └──────────────────────┘
535
536 end add_monoid
537
538 namespace canonically_ordered_semiring
539 variable [canonically_ordered_comm_semiring α]
id └───────────────────────────────┘
src └───────────────────────────────┘
typ └───────────────────────────────┘
540
541 theorem pow_pos {a : α} (H : 0 < a) : ∀ n : ℕ, 0 < a ^ n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
542 | 0 := canonically_ordered_semiring.zero_lt_one
id └──────────────────────────────────────┘
src └──────────────────────────────────────┘
typ └──────────────────────────────────────┘
doc └──────────────────────────────────────┘
543 | (n+1) := canonically_ordered_semiring.mul_pos.2 ⟨H, pow_pos n⟩
id ┴┴ └──────────────────────────────────┘┴ ┴ └─────┘
src ┴ └──────────────────────────────────┘┴
typ ┴┴ └──────────────────────────────────┘┴ ┴ └─────┘
544
545 lemma pow_le_pow_of_le_left {a b : α} (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
546 | 0 := by simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
547 | (k+1) := canonically_ordered_semiring.mul_le_mul hab (pow_le_pow_of_le_left k)
id ┴┴ └─────────────────────────────────────┘ └─┘ └───────────────────┘
src ┴ └─────────────────────────────────────┘
typ ┴┴ └─────────────────────────────────────┘ └─┘ └───────────────────┘
548
549 theorem one_le_pow_of_one_le {a : α} (H : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
550 by simpa only [one_pow] using pow_le_pow_of_le_left H n
id └─────┘ └───────────────────┘ ┴ ┴
src └──────────┘└─────┘└──────┘└───────────────────┘┴ ┴ └
typ └──────────┘└─────┘└──────┘└───────────────────┘┴┴┴┴└
doc └──────────┘ └──────┘ ┴ ┴ └
txt └──────────┘ └──────┘ ┴ ┴ └
par └──────────┘ └──────┘ ┴ ┴ └
pid ┴└──┘└┘ ┴┴└────┘ ┴ ┴ └
st └─────────────────────────────────────────────────────
551
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
552 theorem pow_le_one {a : α} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1:=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
553 by simpa only [one_pow] using pow_le_pow_of_le_left H n
id └─────┘ └───────────────────┘ ┴ ┴
src └──────────┘└─────┘└──────┘└───────────────────┘┴ ┴ └
typ └──────────┘└─────┘└──────┘└───────────────────┘┴┴┴┴└
doc └──────────┘ └──────┘ ┴ ┴ └
txt └──────────┘ └──────┘ ┴ ┴ └
par └──────────┘ └──────┘ ┴ ┴ └
pid ┴└──┘└┘ ┴┴└────┘ ┴ ┴ └
st └─────────────────────────────────────────────────────
554
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
555 end canonically_ordered_semiring
556
557 section linear_ordered_semiring
558 variable [linear_ordered_semiring α]
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
559
560 theorem pow_pos {a : α} (H : 0 < a) : ∀ (n : ℕ), 0 < a ^ n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
561 | 0 := zero_lt_one
id └─────────┘
src └─────────┘
typ └─────────┘
562 | (n+1) := mul_pos H (pow_pos _)
id ┴ └─────┘ ┴ └─────┘
src ┴ └─────┘
typ ┴ └─────┘ ┴ └─────┘
563
564 theorem pow_nonneg {a : α} (H : 0 ≤ a) : ∀ (n : ℕ), 0 ≤ a ^ n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
565 | 0 := zero_le_one
id └─────────┘
src └─────────┘
typ └─────────┘
566 | (n+1) := mul_nonneg H (pow_nonneg _)
id ┴ └────────┘ ┴ └────────┘
src ┴ └────────┘
typ ┴ └────────┘ ┴ └────────┘
567
568 theorem pow_lt_pow_of_lt_left {x y : α} {n : ℕ} (Hxy : x < y) (Hxpos : 0 ≤ x) (Hnpos : 0 < n) : x ^ n < y ^ n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
569 begin
st └─────
570 cases lt_or_eq_of_le Hxpos,
id └────────────┘ └───┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴└───┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────┘└─
571 { rw ←nat.sub_add_cancel Hnpos,
id └────────────────┘ └───┘
src └──┘└────────────────┘┴
typ └──┘└────────────────┘┴└───┘
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───┘└──────────────────────────┘└─
572 induction (n - 1), { simpa only [pow_one] },
id ┴ ┴ └─────┘
src └────────┘ ┴┴└─┘ └──────────┘└─────┘└┘
typ └────────┘ ┴┴┴└─┘ └──────────┘└─────┘└┘
doc └────────┘ ┴ └─┘ └──────────┘ └┘
txt └────────┘ ┴ └─┘ └──────────┘ └┘
par └────────┘ ┴ └─┘ └──────────┘ └┘
pid ┴ ┴ └─┘ ┴└──┘└┘ ┴┴
st ────────────────────┘└──┘└───────────────────┘└┘└
573 rw [pow_add, pow_add, nat.succ_eq_add_one, pow_one, pow_one],
id └─────┘ └─────┘ └─────────────────┘ └─────┘ └─────┘
src └──┘└─────┘└┘└─────┘└┘└─────────────────┘└┘└─────┘└┘└─────┘┴
typ └──┘└─────┘└┘└─────┘└┘└─────────────────┘└┘└─────┘└┘└─────┘┴
doc └──┘ └┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴
st ──────────────┘└───────┘└───────────────────┘└───────┘└───────┘┴└─
574 apply mul_lt_mul ih (le_of_lt Hxy) h (le_of_lt (pow_pos (lt_trans h Hxy) _)) },
id └────────┘ └┘ └──────┘ └─────┘ └──────┘ ┴ └─┘
src └────┘└────────┘┴ ┴ ┴ └┘ ┴ └──────┘┴ └─────┘┴ └──────┘┴ ┴ └────┘
typ └────┘└────────┘┴└┘┴ ┴ └┘ ┴ └──────┘┴ └─────┘┴ └──────┘┴┴┴└─┘└────┘
doc └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └────┘
txt └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └────┘
par └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘┴
st ────────────────────────────────────────────────────────────────────────────────┘└┘└
575 { rw [←h, zero_pow Hnpos], apply pow_pos (by rwa ←h at Hxy : 0 < y),}
id ┴ └──────┘ └───┘ └─────┘ ┴ ┴ ┴
src └───┘ └┘└──────┘┴ ┴ └────┘└─────┘┴ ┴└───┘ └──────┘└──┘┴┴ ┴
typ └───┘┴└┘└──────┘┴└───┘┴ └────┘└─────┘┴ ┴└───┘┴└──────┘└──┘┴┴┴┴
doc └───┘ └┘ ┴ ┴ └────┘ ┴ ┴└───┘ └──────┘└──┘ ┴ ┴
txt └───┘ └┘ ┴ ┴ └────┘ ┴ ┴└───┘ └──────┘└──┘ ┴ ┴
par └───┘ └┘ ┴ ┴ └────┘ ┴ ┴└───┘ └──────┘└──┘ ┴ ┴
pid └─┘ └┘ ┴ ┴ ┴ ┴ └────┘ └──────────┘ ┴ ┴
st ─────────┘└──────────────┘┴└─────────────────┘└─────────────┘└──────┘└──
576 end
st ──┘
577
578 theorem pow_right_inj {x y : α} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) (Hxyn : x ^ n = y ^ n) : x = y :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
579 begin
st └─────
580 rcases lt_trichotomy x y with hxy | rfl | hyx,
id └───────────┘ ┴ ┴
src └─────┘└───────────┘┴ ┴ └───────────────────┘
typ └─────┘└───────────┘┴┴┴┴└───────────────────┘
doc └─────┘ ┴ ┴ └───────────────────┘
txt └─────┘ ┴ ┴ └───────────────────┘
par └─────┘ ┴ ┴ └───────────────────┘
pid ┴ ┴ ┴ └───────────────────┘
st ──────────────────────────────────────────────┘└─
581 { exact absurd Hxyn (ne_of_lt (pow_lt_pow_of_lt_left hxy Hxpos Hnpos)) },
id └────┘ └──┘ └──────┘ └───────────────────┘ └─┘ └───┘ └───┘
src └────┘└────┘┴ ┴ └──────┘┴ └───────────────────┘┴ ┴ ┴ └─┘
typ └────┘└────┘┴└──┘┴ └──────┘┴ └───────────────────┘┴└─┘┴└───┘┴└───┘└─┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴
st ───┘└───────────────────────────────────────────────────────────────────┘└┘└
582 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
583 { exact absurd Hxyn (ne_of_gt (pow_lt_pow_of_lt_left hyx Hypos Hnpos)) },
id └────┘ └──┘ └──────┘ └───────────────────┘ └─┘ └───┘ └───┘
src └────┘└────┘┴ ┴ └──────┘┴ └───────────────────┘┴ ┴ ┴ └─┘
typ └────┘└────┘┴└──┘┴ └──────┘┴ └───────────────────┘┴└─┘┴└───┘┴└───┘└─┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴
st ────────────────────────────────────────────────────────────────────────┘└──
584 end
st ──┘
585
586 theorem one_le_pow_of_one_le {a : α} (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
587 | 0 := le_refl _
id └─────┘
src └─────┘
typ └─────┘
588 | (n+1) := by simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le n)
id ┴ └─────┘ └────────┘ └──────────────────┘ ┴
src ┴ └──────────┘└─────┘└──────┘└────────┘┴ ┴ ┴ └─
typ ┴ └──────────┘└─────┘└──────┘└────────┘┴ ┴ └──────────────────┘┴┴└─
doc └──────────┘ └──────┘ ┴ ┴ ┴ └─
txt └──────────┘ └──────┘ ┴ ┴ ┴ └─
par └──────────┘ └──────┘ ┴ ┴ ┴ └─
pid ┴└──┘└┘ ┴┴└────┘ ┴ ┴ ┴ └─
st └─────────────────────────────────────────────────────────────────
589 zero_le_one (le_trans zero_le_one H)
id └──────┘ └─────────┘ ┴
src ───┘ ┴ └──────┘┴└─────────┘┴ └─
typ ───┘ ┴ └──────┘┴└─────────┘┴┴└─
doc ───┘ ┴ ┴ ┴ └─
txt ───┘ ┴ ┴ ┴ └─
par ───┘ ┴ ┴ ┴ └─
pid ───┘ ┴ ┴ ┴ ┴└
st ─────────────────────────────────────────
590
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
591 /-- Bernoulli's inequality. This version works for semirings but requires
592 an additional hypothesis `0 ≤ a * a`. -/
593 theorem one_add_mul_le_pow' {a : α} (Hsqr : 0 ≤ a * a) (H : 0 ≤ 1 + a) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
594 ∀ (n : ℕ), 1 + n • a ≤ (1 + a) ^ n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
595 | 0 := le_of_eq $ add_zero _
id └──────┘ └──────┘
src └──────┘ └──────┘
typ └──────┘ └──────┘
596 | (n+1) :=
id ┴┴
src ┴
typ ┴┴
597 calc 1 + (n + 1) • a ≤ (1 + a) * (1 + n • a) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
598 by simpa [succ_smul, mul_add, add_mul, add_monoid.mul_smul_left]
id └───────┘ └─────┘ └─────┘ └──────────────────────┘
src └─────┘└───────┘└┘└─────┘└┘└─────┘└┘└──────────────────────┘└─
typ └─────┘└───────┘└┘└─────┘└┘└─────┘└┘└──────────────────────┘└─
doc └─────┘ └┘ └┘ └┘ └─
txt └─────┘ └┘ └┘ └┘ └─
par └─────┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ ┴└
st └──────────────────────────────────────────────────────────────
599 using add_monoid.smul_nonneg Hsqr n
id └────────────────────┘ └──┘ ┴
src ─────────┘└────────────────────┘┴ ┴ ┴
typ ─────────┘└────────────────────┘┴└──┘┴┴┴
doc ─────────┘ ┴ ┴ ┴
txt ─────────┘ ┴ ┴ ┴
par ─────────┘ ┴ ┴ ┴
pid ───┘└────┘ ┴ ┴ ┴
st ───────────────────────────────────────┘
600 ... ≤ (1 + a)^(n+1) : mul_le_mul_of_nonneg_left (one_add_mul_le_pow' n) H
id ┴ ┴ ┴ ┴ └───────────────────────┘ └─────────────────┘ ┴
src ┴ ┴ ┴ └───────────────────────┘
typ ┴ ┴ ┴ ┴ └───────────────────────┘ └─────────────────┘ ┴
601
602 theorem pow_le_pow {a : α} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
603 let ⟨k, hk⟩ := nat.le.dest h in
id └─┘ ┴ └─────────┘ ┴
src └─────────┘
typ └─┘ ┴ └─────────┘ ┴
604 calc a ^ n = a ^ n * 1 : (mul_one _).symm
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └──┘
src ┴ ┴ ┴ └─────┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └──┘
605 ... ≤ a ^ n * a ^ k : mul_le_mul_of_nonneg_left
id ┴ ┴ ┴ ┴ ┴ ┴ └───────────────────────┘
src ┴ ┴ ┴ └───────────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────────────┘
606 (one_le_pow_of_one_le ha _)
id └──────────────────┘ └┘
src └──────────────────┘
typ └──────────────────┘ └┘
607 (pow_nonneg (le_trans zero_le_one ha) _)
id └────────┘ └──────┘ └─────────┘ └┘
src └────────┘ └──────┘ └─────────┘
typ └────────┘ └──────┘ └─────────┘ └┘
608 ... = a ^ m : by rw [←hk, pow_add]
id ┴ ┴ ┴ └┘ └─────┘
src ┴ └───┘ └┘└─────┘└─
typ ┴ ┴ ┴ └───┘└┘└┘└─────┘└─
doc └───┘ └┘ └─
txt └───┘ └┘ └─
par └───┘ └┘ └─
pid └─┘ └┘ ┴└
st └──────┘└───────┘┴└
609
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
610 lemma pow_lt_pow {a : α} {n m : ℕ} (h : 1 < a) (h2 : n < m) : a ^ n < a ^ m :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
611 begin
st └─────
612 have h' : 1 ≤ a := le_of_lt h,
id ┴ ┴ └──────┘ ┴
src └──────────┘┴┴ └──┘└──────┘┴
typ └──────────┘┴┴┴└──┘└──────┘┴┴
doc └──────────┘ ┴ └──┘ ┴
txt └──────────┘ ┴ └──┘ ┴
par └──────────┘ ┴ └──┘ ┴
pid └─────┘└───┘ ┴ └──┘ ┴
st ──────────────────────────────┘└─
613 have h'' : 0 < a := lt_trans zero_lt_one h,
id ┴ ┴ └──────┘ └─────────┘ ┴
src └───────────┘┴┴ └──┘└──────┘┴└─────────┘┴
typ └───────────┘┴┴┴└──┘└──────┘┴└─────────┘┴┴
doc └───────────┘ ┴ └──┘ ┴ ┴
txt └───────────┘ ┴ └──┘ ┴ ┴
par └───────────┘ ┴ └──┘ ┴ ┴
pid └──────┘└───┘ ┴ └──┘ ┴ ┴
st ───────────────────────────────────────────┘└─
614 cases m, cases h2, rw [pow_succ, ←one_mul (a ^ n)],
id ┴ └┘ └──────┘ └─────┘ ┴ ┴ ┴
src └────┘ └────┘ └──┘└──────┘└─┘└─────┘┴ ┴┴┴ └┘
typ └────┘┴ └────┘└┘ └──┘└──────┘└─┘└─────┘┴ ┴┴┴┴┴└┘
doc └────┘ └────┘ └──┘ └─┘ ┴ ┴ ┴ └┘
txt └────┘ └────┘ └──┘ └─┘ ┴ ┴ ┴ └┘
par └────┘ └────┘ └──┘ └─┘ ┴ ┴ ┴ └┘
pid ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └┘
st ────────┘└────────┘└────────────┘└────────────────┘┴└─
615 exact mul_lt_mul h (pow_le_pow h' (nat.le_of_lt_succ h2)) (pow_pos h'' _) (le_of_lt h'')
id └────────┘ ┴ └────────┘ └┘ └───────────────┘ └┘ └─────┘ └──────┘ └─┘
src └────┘└────────┘┴ ┴ └────────┘┴ ┴ └───────────────┘┴ └─┘ └─────┘┴ └──┘ └──────┘┴ └┘
typ └────┘└────────┘┴┴┴ └────────┘┴└┘┴ └───────────────┘┴└┘└─┘ └─────┘┴ └──┘ └──────┘┴└─┘└┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────────────────────────────┘
616 end
st └─┘
617
618 lemma pow_le_pow_of_le_left {a b : α} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
619 | 0 := by simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
620 | (k+1) := mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab)
id ┴ └────────┘ └─┘ └───────────────────┘ └────────┘ └┘ └──────┘ └┘ └─┘
src ┴ └────────┘ └────────┘ └──────┘
typ ┴ └────────┘ └─┘ └───────────────────┘ └────────┘ └┘ └──────┘ └┘ └─┘
621
622 lemma lt_of_pow_lt_pow {a b : α} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
623 lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h
id └──────────┘ └┘ └──────────┘ └───────────────────┘ └┘ └┘ ┴
src └──────────┘ └──────────┘ └───────────────────┘
typ └──────────┘ └┘ └──────────┘ └───────────────────┘ └┘ └┘ ┴
624
625 private lemma pow_lt_pow_of_lt_one_aux {a : α} (h : 0 < a) (ha : a < 1) (i : ℕ) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
626 ∀ k : ℕ, a ^ (i + k + 1) < a ^ i
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
627 | 0 := begin simp only [add_zero], rw ←one_mul (a^i), exact mul_lt_mul ha (le_refl _) (pow_pos h _) zero_le_one end
id └──────┘ └─────┘ ┴┴┴ └────────┘ └┘ └─────┘ └─────┘ ┴ └─────────┘
src └─────────┘└──────┘┴ └──┘└─────┘┴ ┴ ┴ └────┘└────────┘┴ ┴ └─────┘└──┘ └─────┘┴ └──┘└─────────┘┴
typ └─────────┘└──────┘┴ └──┘└─────┘┴ ┴┴┴┴ └────┘└────────┘┴└┘┴ └─────┘└──┘ └─────┘┴┴└──┘└─────────┘┴
doc └─────────┘ ┴ └──┘ ┴ ┴ └────┘ ┴ ┴ └──┘ ┴ └──┘ ┴
txt └─────────┘ ┴ └──┘ ┴ ┴ └────┘ ┴ ┴ └──┘ ┴ └──┘ ┴
par └─────────┘ ┴ └──┘ ┴ ┴ └────┘ ┴ ┴ └──┘ ┴ └──┘ ┴
pid ┴└──┘└┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴
st └────────────────────────┘└─────────────────┘└──────────────────────────────────────────────────────────┘└─┘
628 | (k+1) :=
id ┴
src ┴
typ ┴
629 begin
st └─────
630 rw ←one_mul (a^i),
id └─────┘ ┴ ┴
src └──┘└─────┘┴ ┴
typ └──┘└─────┘┴ ┴ ┴┴
doc └──┘ ┴ ┴
txt └──┘ ┴ ┴
par └──┘ ┴ ┴
pid └┘ ┴ ┴
st ────────────────────┘└─
631 apply mul_lt_mul ha _ _ zero_le_one,
id └────────┘ └┘ └─────────┘
src └────┘└────────┘┴ └───┘└─────────┘
typ └────┘└────────┘┴└┘└───┘└─────────┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ──────────────────────────────────────┘└─
632 { apply le_of_lt, apply pow_lt_pow_of_lt_one_aux },
id └──────┘
src └────┘└──────┘ └────┘ ┴
typ └────┘└──────┘ └────┘ ┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴ ┴
st ─────┘└────────────┘└───────────────────────────────┘└┘└
633 { show 0 < a ^ (i + (k + 1) + 0), apply pow_pos h }
id ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─────┘┴┴ ┴ ┴ ┴┴┴ ┴ └──┘ └─┘ └────┘└─────┘┴ ┴
typ └─────┘┴┴┴┴ ┴ ┴┴┴┴ ┴┴ └──┘ └─┘ └────┘└─────┘┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ └────┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ └────┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ └────┘ ┴ ┴
pid └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴
st ───────────────────────────────────┘└────────────────┘└─
634 end
st ────┘
635
636 private lemma pow_le_pow_of_le_one_aux {a : α} (h : 0 ≤ a) (ha : a ≤ 1) (i : ℕ) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
637 ∀ k : ℕ, a ^ (i + k) ≤ a ^ i
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
638 | 0 := by simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
639 | (k+1) := by rw [←add_assoc, ←one_mul (a^i)];
id ┴ └───────┘ └─────┘ ┴┴┴
src ┴ └───┘└───────┘└─┘└─────┘┴ ┴ └┘
typ ┴ └───┘└───────┘└─┘└─────┘┴ ┴┴┴└┘
doc └───┘ └─┘ ┴ └┘
txt └───┘ └─┘ ┴ └┘
par └───┘ └─┘ ┴ └┘
pid └─┘ └─┘ ┴ └┘
st └─────────────┘└──────────────┘┴└─
640 exact mul_le_mul ha (pow_le_pow_of_le_one_aux _) (pow_nonneg h _) zero_le_one
id └────────┘ └┘ └──────────────────────┘ └────────┘ ┴ └─────────┘
src └────┘└────────┘┴ ┴ └──┘ └────────┘┴ └──┘└─────────┘└
typ └────┘└────────┘┴└┘┴ └──────────────────────┘└──┘ └────────┘┴┴└──┘└─────────┘└
doc └────┘ ┴ ┴ └──┘ ┴ └──┘ └
txt └────┘ ┴ ┴ └──┘ ┴ └──┘ └
par └────┘ ┴ ┴ └──┘ ┴ └──┘ └
pid ┴ ┴ ┴ └──┘ ┴ └──┘ └
st ────────────────────────────────────────────────────────────────────────────────────────────
641
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
642 lemma pow_lt_pow_of_lt_one {a : α} (h : 0 < a) (ha : a < 1)
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
643 {i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
644 let ⟨k, hk⟩ := nat.exists_eq_add_of_lt hij in
id └─┘ └─────────────────────┘ └─┘
src └─────────────────────┘
typ └─┘ └─────────────────────┘ └─┘
645 by rw hk; exact pow_lt_pow_of_lt_one_aux h ha _ _
id └┘ └──────────────────────┘ ┴ └┘
src └─┘ └────┘└──────────────────────┘┴ ┴ └────
typ └─┘└┘ └────┘└──────────────────────┘┴┴┴└┘└────
doc └─┘ └────┘ ┴ ┴ └────
txt └─┘ └────┘ ┴ ┴ └────
par └─┘ └────┘ ┴ ┴ └────
pid ┴ ┴ ┴ ┴ └──┘└
st └───────────────────────────────────────────────
646
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
647 lemma pow_le_pow_of_le_one {a : α} (h : 0 ≤ a) (ha : a ≤ 1)
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
648 {i j : ℕ} (hij : i ≤ j) : a ^ j ≤ a ^ i :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
649 let ⟨k, hk⟩ := nat.exists_eq_add_of_le hij in
id └─┘ └─────────────────────┘ └─┘
src └─────────────────────┘
typ └─┘ └─────────────────────┘ └─┘
650 by rw hk; exact pow_le_pow_of_le_one_aux h ha _ _
id └┘ └──────────────────────┘ ┴ └┘
src └─┘ └────┘└──────────────────────┘┴ ┴ └────
typ └─┘└┘ └────┘└──────────────────────┘┴┴┴└┘└────
doc └─┘ └────┘ ┴ ┴ └────
txt └─┘ └────┘ ┴ ┴ └────
par └─┘ └────┘ ┴ ┴ └────
pid ┴ ┴ ┴ ┴ └──┘└
st └───────────────────────────────────────────────
651
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
652 lemma pow_le_one {x : α} : ∀ (n : ℕ) (h0 : 0 ≤ x) (h1 : x ≤ 1), x ^ n ≤ 1
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
653 | 0 h0 h1 := le_refl (1 : α)
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
654 | (n+1) h0 h1 := mul_le_one h1 (pow_nonneg h0 _) (pow_le_one n h0 h1)
id ┴┴ └┘ └┘ └────────┘ └────────┘ └────────┘
src ┴ └────────┘ └────────┘
typ ┴┴ └┘ └┘ └────────┘ └────────┘ └────────┘
655
656 end linear_ordered_semiring
657
658 theorem pow_two_nonneg [linear_ordered_ring α] (a : α) : 0 ≤ a ^ 2 :=
id └─────────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ ┴ ┴
typ └─────────────────┘ ┴ ┴ ┴ ┴ ┴
659 by { rw pow_two, exact mul_self_nonneg _ }
id └─────┘ └─────────────┘
src └─┘└─────┘ └────┘└─────────────┘└─┘
typ └─┘└─────┘ └────┘└─────────────┘└─┘
doc └─┘ └────┘ └─┘
txt └─┘ └────┘ └─┘
par └─┘ └────┘ └─┘
pid ┴ ┴ └┘┴
st └───────────┘└────────────────────────┘└┘
660
661 /-- Bernoulli's inequality for `n : ℕ`, `-2 ≤ a`. -/
662 theorem one_add_mul_le_pow [linear_ordered_ring α] {a : α} (H : -2 ≤ a) :
id └─────────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ ┴ ┴
typ └─────────────────┘ ┴ ┴ ┴ ┴ ┴
663 ∀ (n : ℕ), 1 + n • a ≤ (1 + a) ^ n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
664 | 0 := le_of_eq $ add_zero _
id └──────┘ └──────┘
src └──────┘ └──────┘
typ └──────┘ └──────┘
665 | 1 := by simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
666 | (n+2) :=
id ┴┴
src ┴
typ ┴┴
667 have H' : 0 ≤ 2 + a,
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
668 from neg_le_iff_add_nonneg.1 H,
id └───────────────────┘┴ ┴
src └───────────────────┘┴
typ └───────────────────┘┴ ┴
669 have 0 ≤ n • (a * a * (2 + a)) + a * a,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
670 from add_nonneg (add_monoid.smul_nonneg (mul_nonneg (mul_self_nonneg a) H') n)
id └────────┘ └────────────────────┘ └────────┘ └─────────────┘ ┴ └┘
src └────────┘ └────────────────────┘ └────────┘ └─────────────┘
typ └────────┘ └────────────────────┘ └────────┘ └─────────────┘ ┴ └┘
671 (mul_self_nonneg a),
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
672 calc 1 + (n + 2) • a ≤ 1 + (n + 2) • a + (n • (a * a * (2 + a)) + a * a) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
673 (le_add_iff_nonneg_right _).2 this
id └─────────────────────┘ ┴ └──┘
src └─────────────────────┘ ┴
typ └─────────────────────┘ ┴ └──┘
674 ... = (1 + a) * (1 + a) * (1 + n • a) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
675 by { simp only [add_mul, mul_add, mul_two, mul_one, one_mul, succ_smul, add_monoid.smul_add,
id └─────┘ └─────┘ └─────┘ └─────┘ └─────┘ └───────┘ └─────────────────┘
src └─────────┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└─────────────────┘└─
typ └─────────┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└─────────────────┘└─
doc └─────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
st └──────────────────────────────────────────────────────────────────────────────────────────
676 add_monoid.mul_smul_assoc, (add_monoid.mul_smul_left _ _ _).symm],
id └───────────────────────┘ └──────────────────────┘
src ────────┘└───────────────────────┘└┘ └──────────────────────┘└───────────┘
typ ────────┘└───────────────────────┘└┘ └──────────────────────┘└───────────┘
doc ────────┘ └┘ └───────────┘
txt ────────┘ └┘ └───────────┘
par ────────┘ └┘ └───────────┘
pid ────────┘ └┘ └───────────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
677 ac_refl }
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────────┘└┘
678 ... ≤ (1 + a) * (1 + a) * (1 + a)^n :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
679 mul_le_mul_of_nonneg_left (one_add_mul_le_pow n) (mul_self_nonneg (1 + a))
id └───────────────────────┘ └────────────────┘ └─────────────┘ ┴ ┴
src └───────────────────────┘ └─────────────┘ ┴
typ └───────────────────────┘ └────────────────┘ └─────────────┘ ┴ ┴
680 ... = (1 + a)^(n + 2) : by simp only [pow_succ, mul_assoc]
id ┴ ┴ ┴ ┴ └──────┘ └───────┘
src ┴ ┴ ┴ └─────────┘└──────┘└┘└───────┘└─
typ ┴ ┴ ┴ ┴ └─────────┘└──────┘└┘└───────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────
681
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
682 /-- Bernoulli's inequality reformulated to estimate `a^n`. -/
683 theorem one_add_sub_mul_le_pow [linear_ordered_ring α]
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
684 {a : α} (H : -1 ≤ a) (n : ℕ) : 1 + n • (a - 1) ≤ a ^ n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
685 have -2 ≤ a - 1, by { rw [bit0, neg_add], exact sub_le_sub_right H 1 },
id ┴ ┴ ┴ ┴ └──┘ └─────┘ └──────────────┘ ┴
src ┴ ┴ ┴ └──┘└──┘└┘└─────┘┴ └────┘└──────────────┘┴ └─┘
typ ┴ ┴ ┴ ┴ └──┘└──┘└┘└─────┘┴ └────┘└──────────────┘┴┴└─┘
doc └──┘ └┘ ┴ └────┘ ┴ └─┘
txt └──┘ └┘ ┴ └────┘ ┴ └─┘
par └──┘ └┘ ┴ └────┘ ┴ └─┘
pid └┘ └┘ ┴ ┴ ┴ ┴└┘
st └─────────┘└───────┘└────────────────────────────┘└┘
686 by simpa only [add_sub_cancel'_right] using one_add_mul_le_pow this n
id └───────────────────┘ └────────────────┘ └──┘ ┴
src └──────────┘└───────────────────┘└──────┘└────────────────┘┴ ┴ └
typ └──────────┘└───────────────────┘└──────┘└────────────────┘┴└──┘┴┴└
doc └──────────┘ └──────┘└────────────────┘┴ ┴ └
txt └──────────┘ └──────┘ ┴ ┴ └
par └──────────┘ └──────┘ ┴ ┴ └
pid ┴└──┘└┘ ┴┴└────┘ ┴ ┴ └
st └───────────────────────────────────────────────────────────────────
687
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
688 namespace int
689
690 lemma units_pow_two (u : units ℤ) : u ^ 2 = 1 :=
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴
691 (units_eq_one_or u).elim (λ h, h.symm ▸ rfl) (λ h, h.symm ▸ rfl)
id └─────────────┘ ┴ └──┘ ┴ ┴└───┘ ┴ └─┘ ┴ ┴└───┘ ┴ └─┘
src └─────────────┘ └──┘ └───┘ ┴ └─┘ └───┘ ┴ └─┘
typ └─────────────┘ ┴ └──┘ ┴ ┴└───┘ ┴ └─┘ ┴ ┴└───┘ ┴ └─┘
692
693 lemma units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) : u ^ n = u ^ (n % 2) :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
694 by conv {to_lhs, rw ← nat.mod_add_div n 2}; rw [pow_add, pow_mul, units_pow_two, one_pow, mul_one]
id └─────────────┘ ┴ └─────┘ └─────┘ └───────────┘ └─────┘ └─────┘
src └────┘└────┘└┘└───┘└─────────────┘┴ └┘┴ └──┘└─────┘└┘└─────┘└┘└───────────┘└┘└─────┘└┘└─────┘└─
typ └────┘└────┘└┘└───┘└─────────────┘┴┴└┘┴ └──┘└─────┘└┘└─────┘└┘└───────────┘└┘└─────┘└┘└─────┘└─
doc └──┘ └┘ └┘ └┘ └┘ └─
txt └────┘└────┘└┘└───┘ ┴ └┘┴ └──┘ └┘ └┘ └┘ └┘ └─
par └────┘└────┘└┘└───┘ ┴ └┘┴ └──┘ └┘ └┘ └┘ └┘ └─
pid ┴└────────────┘ ┴ └─┘ └┘ └┘ └┘ └┘ └┘ ┴└
st └─────┘└────┘└────────────────────────┘└┘└───┘└─────┘└───────┘└─────────────┘└───────┘└───────┘┴└
695
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
696 end int
697
698 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
id └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴┴
doc └──┘
699 by simp [pow, monoid.pow]
id └────────┘
src └────┘ └┘└────────┘└─
typ └────┘ └┘└────────┘└─
doc └────┘ └┘└────────┘└─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └───────────────────────
700
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
701 lemma div_sq_cancel {α} [field α] {a : α} (ha : a ≠ 0) (b : α) : a^2 * b / a = a * b :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
702 by rw [pow_two, mul_assoc, mul_div_cancel_left _ ha]
id └─────┘ └───────┘ └─────────────────┘ └┘
src └──┘└─────┘└┘└───────┘└┘└─────────────────┘└─┘ ┴
typ └──┘└─────┘└┘└───────┘└┘└─────────────────┘└─┘└┘┴
doc └──┘ └┘ └┘ └─┘ ┴
txt └──┘ └┘ └┘ └─┘ ┴
par └──┘ └┘ └┘ └─┘ ┴
pid └┘ └┘ └┘ └─┘ ┴
st └──────────┘└─────────┘└────────────────────────┘┴